From 097796f1ebfa4009502e23494af08f332613ace3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:27:25 +0100 Subject: comInductive: remove redundant check_evars calls We do [solve_remaining_evars all_and_fail_flags] immediately before calling [interp_mutual_inductive_constr] so these checks are extra. --- vernac/comInductive.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'vernac/comInductive.mli') diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index ef05b213d8..6ff9d2142b 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -55,7 +55,6 @@ val interp_mutual_inductive_constr : template:bool option -> udecl:UState.universe_decl -> env_ar:Environ.env -> - env_params:Environ.env -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> indnames:Names.Id.t list -> arities:EConstr.t list -> -- cgit v1.2.3 From b621bc02657bd1effcca371b56260b0a7a327ed9 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:36:06 +0100 Subject: reduce arguments of template_polymorphism_candidate take only the template_check flag instead of the whole env --- vernac/comInductive.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'vernac/comInductive.mli') 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. *) -- cgit v1.2.3 From 4f1d657f42957d0c2d115424564eedf599584cbc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:50:47 +0100 Subject: Remove variance info from inductive entries, infer in indtyping It gets thrown away if the inductive is declared in a section anyway, and there is no user syntax to specify it. --- vernac/comInductive.mli | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'vernac/comInductive.mli') diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 73d385dec8..418d971558 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -49,22 +49,22 @@ val declare_mutual_inductive_with_eliminations -> Names.MutInd.t [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] -val interp_mutual_inductive_constr : - sigma:Evd.evar_map -> - template:bool option -> - udecl:UState.universe_decl -> - env_ar:Environ.env -> - ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> - indnames:Names.Id.t list -> - arities:EConstr.t list -> - arityconcl:(bool * EConstr.ESorts.t) option list -> - constructors:(Names.Id.t list * Constr.constr list * 'a list list) list -> - env_ar_params:Environ.env -> - cumulative:bool -> - poly:bool -> - private_ind:bool -> - finite:Declarations.recursivity_kind -> - Entries.mutual_inductive_entry * UnivNames.universe_binders +val interp_mutual_inductive_constr + : sigma:Evd.evar_map + -> template:bool option + -> udecl:UState.universe_decl + -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list + -> indnames:Names.Id.t list + -> arities:EConstr.t list + -> arityconcl:(bool * EConstr.ESorts.t) option list + -> constructors:(Names.Id.t list * Constr.constr list * 'a list list) list + -> env_ar_params:Environ.env + (** Environment with the inductives and parameters in the rel_context *) + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> finite:Declarations.recursivity_kind + -> Entries.mutual_inductive_entry * UnivNames.universe_binders (************************************************************************) (** Internal API, exported for Record *) -- cgit v1.2.3 From 82a1f73aa6c70672e212f9122c325425f9129570 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 14:05:24 +0100 Subject: Don't pass (ignored) implicits to interp_mutual_inductive_constr --- vernac/comInductive.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comInductive.mli') diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 418d971558..cc104b3762 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -57,7 +57,7 @@ val interp_mutual_inductive_constr -> indnames:Names.Id.t list -> arities:EConstr.t list -> arityconcl:(bool * EConstr.ESorts.t) option list - -> constructors:(Names.Id.t list * Constr.constr list * 'a list list) list + -> constructors:(Names.Id.t list * Constr.constr list) list -> env_ar_params:Environ.env (** Environment with the inductives and parameters in the rel_context *) -> cumulative:bool -- cgit v1.2.3