diff options
| author | Gaëtan Gilbert | 2019-10-29 13:27:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:48:53 +0100 |
| commit | 097796f1ebfa4009502e23494af08f332613ace3 (patch) | |
| tree | 8c484cca87b6a647804e3bc760932f284902373e /vernac/comInductive.mli | |
| parent | 62adf2b9e03afa212fcd8819226da068bf4a32b8 (diff) | |
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.
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 1 |
1 files changed, 0 insertions, 1 deletions
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 -> |