diff options
| author | Gaëtan Gilbert | 2019-10-29 13:36:06 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:52:46 +0100 |
| commit | b621bc02657bd1effcca371b56260b0a7a327ed9 (patch) | |
| tree | 9bcd17cd98b44b342ca455cfd7ca92adc462dc29 /vernac/comInductive.mli | |
| parent | 097796f1ebfa4009502e23494af08f332613ace3 (diff) | |
reduce arguments of template_polymorphism_candidate
take only the template_check flag instead of the whole env
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 6ff9d2142b..73d385dec8 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -50,7 +50,6 @@ val declare_mutual_inductive_with_eliminations [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] val interp_mutual_inductive_constr : - env0:Environ.env -> sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> @@ -77,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : Environ.env + : template_check:bool -> ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env ~ctor_levels uctx params +(** [template_polymorphism_candidate ~template_check ~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 + conclusion sort, if one is given. If the [template_check] flag is false we just check that the conclusion sort is not small. *) |