diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 16 | ||||
| -rw-r--r-- | printing/printer.ml | 8 | ||||
| -rw-r--r-- | printing/printer.mli | 2 |
3 files changed, 22 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f82b9cef68..b7fefca22b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -221,14 +221,22 @@ let print_if_is_coercion ref = (*******************) (* *) +let pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - [ pr_global ref ++ str " is " ++ str - (if poly then "universe polymorphic" + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" else if template_poly then - "template universe polymorphic" - else "not universe polymorphic") ] + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] let print_type_in_type ref = let unsafe = Global.is_type_in_type ref in diff --git a/printing/printer.ml b/printing/printer.ml index e3225fadd5..328082fbc2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -854,6 +854,8 @@ 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 GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -873,10 +875,13 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 + | TemplatePolymorphic m1, TemplatePolymorphic m2 -> + MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 + | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -937,6 +942,9 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TemplatePolymorphic m -> + hov 2 (safe_pr_inductive env m ++ spc () ++ + strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 788f303aee..d62d3789d3 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -192,6 +192,8 @@ 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 GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = |