diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index cbdc84e073..e9c347c9bb 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -315,7 +315,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu in - if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then + let accu = + if cb.const_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType kn, l)) Constr.mkProp accu + in + if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu |