diff options
| author | Pierre-Marie Pédrot | 2020-05-12 12:02:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 12:07:43 +0200 |
| commit | d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 (patch) | |
| tree | fa0648deb47650cc0d026ecdd711c093d36e585c /pretyping | |
| parent | e802f48faf7a472000e218c7a3321c10c2171e0f (diff) | |
Do not use Unsafe.to_constr for old refiner conclusion.
This was useless, since we did not observe the difference on evars.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c7110d7a91..e77c5082dd 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -614,7 +614,7 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf = let set_names env sigma n brty = let open EConstr in let (ctxt,cl) = decompose_prod_n_assum sigma n brty in - EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt) + Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -631,11 +631,12 @@ let type_case_branches_with_names env sigma indspec p c = let nparams = mib.mind_nparams in let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in + let lbrty = Array.map EConstr.of_constr lbrty in (* Build case type *) let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then - (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty) + (set_pattern_names env sigma (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ab69629595..2bec86599e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,7 +194,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : - env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> EConstr.types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info |