diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f3fc46c12..5f2b352a9c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1458,7 +1458,10 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in + let t = Flags.without_option Detyping.print_universes (fun () -> + Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t) + () + in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |