diff options
| author | Gaëtan Gilbert | 2021-01-11 12:12:45 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-01-11 12:13:00 +0100 |
| commit | 925794c34d08752cee85362d1c2772559e89d2c9 (patch) | |
| tree | ea1821bb86fc0d62b2ac09b9fe0650fc9d97070a /vernac | |
| parent | 27a9a28e8628c94910a08efc2f611e91e3e553bb (diff) | |
Fix #13732: Implicit Type vs universes
This returns to the previous behaviour of Implicit Type forgetting
universes.
`Implicit Type T : Type@{u}.` may be confusing as it is equivalent to
`: Type`, but until we have a better idea of what to do with anonymous
types I see no other solution, especially in the short term to fix the
bug.
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 |