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 | |
| 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.
| -rw-r--r-- | vernac/comInductive.ml | 9 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 1 |
2 files changed, 2 insertions, 8 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2afb5e9d65..812bf7b021 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -353,7 +353,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = +let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in @@ -369,11 +369,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 sigma (EConstr.of_constr c)) ctx_params; - List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params sigma (EConstr.of_constr c)) ctyps) - constructors; (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> @@ -509,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) 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 -> |