Merge PR #6874: [econstr] Some minor tweaks

4 files changed, 23 insertions, 17 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0b0e629ab..c8fd0b7a7 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
       if metas then eqclause
       else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
     in
-    let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+    let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
     let rec split_last_two = function
       | [c1;c2] -> [],(c1, c2)
       | x::y::z ->
@@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
       | _ -> raise Not_found
     in
       try
-	let others,(c1,c2) = split_last_two args in
-	let ty1, ty2 =
-	  Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
-	in
-	let ty = EConstr.Unsafe.to_constr ty in
-	let ty1 = EConstr.Unsafe.to_constr ty1 in
+        let others,(c1,c2) = split_last_two args in
+        let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+        (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
+        let open EConstr in
+        let hyp_ty = Unsafe.to_constr ty in
+        let hyp_car = Unsafe.to_constr ty1 in
+        let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in
+        let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in
+        let hyp_left = Unsafe.to_constr @@ c1 in
+        let hyp_right = Unsafe.to_constr @@ c2 in
 (* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
 (* 	  else *)
-	    Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
-		   hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
-		   hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+        Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; }
       with Not_found -> None
   in
     match find_rel ctype with
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index eede13329..ad5239116 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -108,9 +108,14 @@ let get_coq_eq ctx =
     user_err Pp.(str "eq not found.")
 
 let univ_of_eq env eq =
-  let eq = EConstr.of_constr eq in
-  match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
-  | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
+  let open EConstr in
+  let eq = of_constr eq in
+  let sigma = Evd.from_env env in
+  match kind sigma (Retyping.get_type_of env sigma eq) with
+  | Prod (_,t,_) -> (match kind sigma t with
+                       Sort k ->
+                        (match ESorts.kind sigma k with Type u -> u | _ -> assert false)
+                     | _ -> assert false)
   | _ -> assert false
 
 (**********************************************************************)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 339abbc2e..102b8e54d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -293,7 +293,7 @@ let error_too_many_names pats =
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
     str ": " ++ pr_enum (Miscprint.pr_intro_pattern
-                           (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
+                           (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++
     str ".")
 
 let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f47e6b2cd..10937322e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
-  let invProof = EConstr.Unsafe.to_constr invProof in
-  let p = Evarutil.nf_evars_universes sigma invProof in
-    p, sigma
+  let p = EConstr.to_constr sigma invProof in
+  p, sigma
 
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in