diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2bfd67f6f..92359420e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Term -open Environ open EConstr open Vars open Inductiveops @@ -421,7 +420,9 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [Loc.tag @@ Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] + then + let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in + [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -433,7 +434,8 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (Loc.tag @@ Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) + let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in + GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) let detype_instance sigma l = let l = EInstance.kind sigma l in @@ -694,7 +696,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 t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = |