diff options
| author | SimonBoulier | 2019-06-03 16:04:54 +0200 |
|---|---|---|
| committer | SimonBoulier | 2019-08-16 11:43:51 +0200 |
| commit | 889603e7a2ed41b890e43729aa0abf90bebd3ca6 (patch) | |
| tree | 605984cd5ea6bfb6758c87ae9582d8230b825e59 | |
| parent | abab878b8d8b5ca85a4da688abed68518f0b17bd (diff) | |
Improve [Print Assumptions] for type-in-type and assumed positive.
| -rw-r--r-- | printing/printer.ml | 7 | ||||
| -rw-r--r-- | printing/printer.mli | 1 | ||||
| -rw-r--r-- | vernac/assumptions.ml | 8 |
3 files changed, 13 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 9c74d8cfbb..b8f25eb380 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -854,6 +854,7 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of Constant.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -927,9 +928,11 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded kn -> - hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is assumed to be guarded.") + | TypeInType kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in let fold t typ accu = let (v, a, o, tr) = accu in diff --git a/printing/printer.mli b/printing/printer.mli index 0855f2d109..f397b2b643 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -192,6 +192,7 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of Constant.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) 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 |