Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

1 files changed, 6 insertions, 6 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 77a7f006b7..b5a42b3078 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,7 +115,7 @@ let pf_get_new_ids idl g =
 
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_type_of gls c)
+    (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -400,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    thin to_intros;
 	    h_intros to_intros;
 	    (fun g' -> 
-	      let ty_teq = pf_type_of g' (mkVar heq) in
+	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
 		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
@@ -514,13 +514,13 @@ let rec prove_lt hyple g =
       in
       let h =
 	List.find (fun id ->
-          match decompose_app (pf_type_of g (mkVar id)) with
+          match decompose_app (pf_unsafe_type_of g (mkVar id)) with
             | _, t::_ -> eq_constr t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
+	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
       observe_tclTHENLIST (str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
@@ -655,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
 let pf_type c tac gl = 
-  let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
 let pf_typel l tac =
@@ -680,7 +680,7 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_type_of g expr in
+  let type_of_expr = pf_unsafe_type_of g expr in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->