From d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:02:23 +0200
Subject: Do not use Unsafe.to_constr for old refiner conclusion.

This was useless, since we did not observe the difference on evars.
---
 pretyping/inductiveops.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

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 *)
-- 
cgit v1.2.3