diff options
| author | Pierre-Marie Pédrot | 2020-02-07 18:13:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-09 16:38:14 +0100 |
| commit | b6264bb2df9b73b905af126ede49cd31abf0e7da (patch) | |
| tree | 6eddb39c2870eb12be6d6cdb5cfe15f9eaf55513 /printing | |
| parent | 1820f40590ec358b40e3a9c444f80c5283e55292 (diff) | |
Remove the Template Check option.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 8 | ||||
| -rw-r--r-- | printing/printer.mli | 2 |
2 files changed, 0 insertions, 10 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 97e0528939..8af4d1d932 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -859,8 +859,6 @@ 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 = @@ -880,13 +878,10 @@ 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 = @@ -947,9 +942,6 @@ 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 1d7a25cbb6..cd5151bd8f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -231,8 +231,6 @@ 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 = |