Do not use Unsafe.to_constr for old refiner conclusion.

This was useless, since we did not observe the difference on evars.

5 files changed, 12 insertions, 12 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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 406e71aafc..4eb8658f83 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,7 +28,7 @@ module NamedDecl = Context.Named.Declaration
 type refiner_error =
 
   (* Errors raised by the refiner *)
-  | BadType of constr * constr * constr
+  | BadType of constr * constr * EConstr.t
   | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
   | NotWellTyped of constr
@@ -318,7 +318,7 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in
     match ans with
     | Some evm -> evm
     | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
@@ -354,7 +354,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     else
       match kind trm with
       | Meta _ ->
-        let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
+        let conclty = nf_betaiota env sigma conclty in
           if !check && occur_meta sigma conclty then
             raise (RefinerError (env, sigma, MetaInType conclty));
           let (gl,ev,sigma) = mk_goal hyps conclty in
@@ -365,7 +365,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | Cast (t,k, ty) ->
         let sigma = check_typability env sigma ty in
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
-        let res = mk_refgoals sigma goal goalacc ty t in
+        let res = mk_refgoals sigma goal goalacc (EConstr.of_constr ty) t in
         (* we keep the casts (in particular VMcast and NATIVEcast) except
            when they are annotating metas *)
         if isMeta t then begin
@@ -437,7 +437,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | Cast (t,_, ty) ->
         let sigma = check_typability env sigma ty in
-        mk_refgoals sigma goal goalacc ty t
+        mk_refgoals sigma goal goalacc (EConstr.of_constr ty) t
 
     | App (f,l) ->
         let (acc',hdty,sigma,applicand) =
@@ -485,7 +485,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
     let t = collapse t in
     match kind t with
     | Prod (_, c1, b) ->
-      let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
+      let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc (EConstr.of_constr c1) harg in
       (acc, subst1 harg b, sigma), arg
     | _ ->
       let env = Goal.V82.env sigma goal in
@@ -577,7 +577,6 @@ let convert_hyp ~check ~reorder env sigma d =
 let prim_refiner r sigma goal =
   let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
-  let cl = EConstr.Unsafe.to_constr cl in
   check_meta_variables env sigma r;
   let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
   let sgl = List.rev sgl in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ef8b2731b2..5d21474394 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -33,7 +33,7 @@ val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal li
 type refiner_error =
 
   (*i Errors raised by the refiner i*)
-  | BadType of constr * constr * constr
+  | BadType of constr * constr * EConstr.t
   | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
   | NotWellTyped of constr
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 41f2ab9c63..4fe3f07d6e 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function
 (* Refiner errors *)
 
 let explain_refiner_bad_type env sigma arg ty conclty =
-  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
+  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in
   str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr_env env sigma arg ++ spc () ++
   str "of type" ++ brk(1,1) ++ pm ++ spc () ++