From b6264bb2df9b73b905af126ede49cd31abf0e7da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 18:13:25 +0100
Subject: Remove the Template Check option.

---
 vernac/comInductive.mli | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'vernac/comInductive.mli')

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index cc104b3762..1286e4a5c3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool
    inductive under consideration. *)
 
 val template_polymorphism_candidate
-  : template_check:bool
-  -> ctor_levels:Univ.LSet.t
+  : ctor_levels:Univ.LSet.t
   -> Entries.universes_entry
   -> Constr.rel_context
   -> Sorts.t option
   -> bool
-(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
+(** [template_polymorphism_candidate ~ctor_levels uctx params
    conclsort] is [true] iff an inductive with params [params],
    conclusion [conclsort] and universe levels appearing in the
    constructor arguments [ctor_levels] would be definable as template
    polymorphic. It should have at least one universe in its
    monomorphic universe context that can be made parametric in its
-   conclusion sort, if one is given. If the [template_check] flag is
-   false we just check that the conclusion sort is not small. *)
+   conclusion sort, if one is given. *)
-- 
cgit v1.2.3