The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Abhishek,

I attach a patch which implements your request. You could e.g. submit
it as a pull request on https://github.com/coq/coq/pulls to collect
opinions on whether this change gets support.

Best,

Hugo

On Thu, Jan 19, 2017 at 01:10:27PM -0500, Abhishek Anand wrote:
> Is there a switch to enable printing types of let bindings?
> For example:
> 
> Definition xx :nat := 
> let x:=0 in x.
> 
> When I say Print xx,
> I want to see
> xx =  let x: nat :=0 in x
> instead of 
> xx =  let x :=0 in x
> 
> I tried "Set Printing All" (in the CoqIDE menu), but I don't see those 
> types.
> IIUC, those types are already available in the kernel (constr.ml) and the
> printing function discards them.
> 
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 85125a5..92b1855 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env 
sigma na body ty c =
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when 
!Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of 
sigma missing in debugger *) in
-      let c = if s != InProp then c else
+      let c = if s != InProp && not !Flags.raw_print then c else
           GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
       GLetIn (dl, na', c, r)