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/printer.mli | |
| parent | 1820f40590ec358b40e3a9c444f80c5283e55292 (diff) | |
Remove the Template Check option.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 2 |
1 files changed, 0 insertions, 2 deletions
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 = |