Tactics API using EConstr.

7 files changed, 112 insertions, 93 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b674f40e9..503cafdd5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -175,6 +175,7 @@ let is_incompatible_eq t =
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
+  let t = EConstr.of_constr t in
   fun g ->
     let prov_id = pf_get_new_id hyp_id g in
     tclTHENS
@@ -451,6 +452,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			      )
 		     in
 		     let to_refine = EConstr.of_constr to_refine in
+		     let t_x = EConstr.of_constr t_x in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
 		       (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
@@ -644,7 +646,8 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in
+	  let c = EConstr.of_constr c in
+	  let evm, _ = pf_apply Typing.type_of g c in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -709,13 +712,14 @@ let build_proof
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
+		  let term_eq = EConstr.of_constr term_eq in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
+		      Proofview.V82.of_tactic (generalize (term_eq::(List.map EConstr.mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
-		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
+		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],EConstr.of_constr t] None);
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
+			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case (EConstr.of_constr t));
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -942,7 +946,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN
-    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map mkVar to_revert) )))
+    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map EConstr.mkVar to_revert) )))
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
@@ -950,7 +954,7 @@ let id_of_decl = RelDecl.get_name %> Nameops.out_name
 let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
-    (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
+    (Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar idl)))
     (thin idl)
 
 let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
@@ -991,7 +995,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
-	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
+	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
@@ -1064,10 +1068,11 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic =
   fun g ->
   let princ_type = pf_concl g in
+  let princ_type = EConstr.of_constr princ_type in
   (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
   (* Pp.msgnl (str "all_funs "); *)
   (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
-    let princ_info = compute_elim_sig princ_type in
+    let princ_info = compute_elim_sig (project g) princ_type in
     let fresh_id =
       let avoid = ref (pf_ids_of_hyps g) in
       (fun na ->
@@ -1227,7 +1232,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	| _, this_fix_info::others_infos ->
 	    let other_fix_infos =
 	      List.map
-		(fun fi -> fi.name,fi.idx + 1 ,fi.types)
+		(fun fi -> fi.name,fi.idx + 1 ,EConstr.of_constr fi.types)
 		(pre_info@others_infos)
 	    in
 	    if List.is_empty other_fix_infos
@@ -1462,11 +1467,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
-	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
+	    (Proofview.V82.of_tactic (apply (EConstr.mkVar hrec)))
 	    [ tclTHENSEQ
 		[
 		  (Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
-		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
+		  (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force acc_inv))));
 		  (fun g ->
 		     if is_mes
 		     then
@@ -1482,7 +1487,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
 				      (true,5)
-				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
 				      [Hints.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
@@ -1518,7 +1523,8 @@ let prove_principle_for_gen
     (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
     rec_arg_num rec_arg_type relation gl =
   let princ_type = pf_concl gl in
-  let princ_info = compute_elim_sig princ_type in
+  let princ_type = EConstr.of_constr princ_type in
+  let princ_info = compute_elim_sig (project gl) princ_type in
   let fresh_id =
     let avoid = ref (pf_ids_of_hyps gl) in
     fun na ->
@@ -1572,7 +1578,7 @@ let prove_principle_for_gen
     Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
-    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
+    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map EConstr.mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
@@ -1580,12 +1586,12 @@ let prove_principle_for_gen
 	 (tclCOMPLETE
 	    (tclTHEN
 	       (Proofview.V82.of_tactic (assert_by (Name wf_thm_id)
-		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
 		  (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
-		 Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])))
+		 Proofview.V82.of_tactic (Tactics.Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))))
 	       )
 	    )
 	 )
@@ -1596,7 +1602,7 @@ let prove_principle_for_gen
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
-     | Some lemma -> lemma
+     | Some lemma -> EConstr.of_constr lemma
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
@@ -1644,7 +1650,7 @@ let prove_principle_for_gen
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
 	 (Name acc_rec_arg_id)
- 	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ 	 (EConstr.of_constr (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])))
 	 (Proofview.V82.tactic prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 4b47b83af..4d88f9f91 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -28,7 +28,8 @@ let observe s =
    a functional one
 *)
 let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
-  let princ_type_info = compute_elim_sig princ_type in
+  let princ_type = EConstr.of_constr princ_type in
+  let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in
   let env = Global.env () in
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
@@ -89,7 +90,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	 (Option.fold_right
 			   mkProd_or_LetIn
 			   princ_type_info.indarg
-			   princ_type_info.concl
+			   (EConstr.Unsafe.to_constr princ_type_info.concl)
 			)
 	 princ_type_info.args
       )
@@ -243,7 +244,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
 let change_property_sort evd toSort princ princName =
   let open Context.Rel.Declaration in
-  let princ_info = compute_elim_sig princ in
+  let princ = EConstr.of_constr princ in
+  let princ_info = compute_elim_sig evd princ in
   let change_sort_in_predicate decl =
     LocalAssum
     (get_name decl,
@@ -270,7 +272,7 @@ let change_property_sort evd toSort princ princName =
 
 let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
-  let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
+  let mutr_nparams = (compute_elim_sig !evd (EConstr.of_constr old_princ_type)).nparams in
   (*   let time1 = System.get_time ()  in *)
   let new_principle_type =
     compute_new_princ_type_from_rel
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a8..a6f971703 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -58,7 +58,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
     | None -> mt ()
     | Some b ->
       let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
-      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
+      spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed (EConstr.Unsafe.to_constr %> prc) (EConstr.Unsafe.to_constr %> prlc) b)
 
 
 ARGUMENT EXTEND fun_ind_using
@@ -97,7 +97,9 @@ ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 | []  ->[ None ]
 END
 
-
+let functional_induction b c x pat =
+  let x = Option.map (Miscops.map_with_bindings EConstr.Unsafe.to_constr) x in
+  Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
 
 
 TACTIC EXTEND newfunind
@@ -108,7 +110,7 @@ TACTIC EXTEND newfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))) princl ]
+       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
@@ -119,7 +121,7 @@ TACTIC EXTEND snewfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x (Option.map out_disjunctive pat))) princl ]
+       Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
 END
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e3ba52246..37a76bec1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -81,7 +81,8 @@ let functional_induction with_clean c princl pat =
       | Some ((princ,binding)) ->
 	 princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g
     in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let princ_type = EConstr.of_constr princ_type in
+    let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
     let args_as_induction_constr =
       let c_list =
 	if princ_infos.Tactics.farg_in_concl
@@ -89,9 +90,11 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
+    let princ = EConstr.of_constr princ in
+    let bindings = Miscops.map_bindings EConstr.of_constr bindings in
     let princ' = Some (princ,bindings) in
     let princ_vars =
       List.fold_right
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b2419b1a5..36fb6dad3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let princ_type = EConstr.of_constr princ_type in
+    let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
@@ -315,7 +316,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 			     match kind_of_term t'',kind_of_term t''' with
 			       | App(eq,args), App(graph',_)
 				   when
-				     (eq_constr eq eq_ind) &&
+				     (Term.eq_constr eq eq_ind) &&
 				       Array.exists  (Constr.eq_constr_nounivs graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
@@ -387,7 +388,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
+				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
 	  ]
       )
 	g
@@ -440,7 +441,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (exact_check f_principle)));
+	  (exact_check (EConstr.of_constr f_principle))));
 	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
@@ -450,7 +451,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
 		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
-		Proofview.V82.of_tactic (apply term) gl')
+		Proofview.V82.of_tactic (apply (EConstr.of_constr term)) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
@@ -467,7 +468,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -495,7 +496,7 @@ and intros_with_rewrite_aux : tactic =
 	  | Prod(_,t,t') ->
 	      begin
 		match kind_of_term t with
-		  | App(eq,args) when (eq_constr eq eq_ind)  ->
+		  | App(eq,args) when (Term.eq_constr eq eq_ind)  ->
  		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
@@ -541,11 +542,11 @@ and intros_with_rewrite_aux : tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
+		  | Ind _ when Term.eq_constr t (Coqlib.build_coq_False ()) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (simplest_case v);
+			Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -582,7 +583,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (simplest_case v);
+	      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -597,7 +598,7 @@ let rec reflexivity_with_destruct_cases g =
 	     None -> tclIDTAC g
 	   | Some id ->
 	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
-		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
+		 | App(eq,[|_;t1;t2|]) when Term.eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
@@ -662,7 +663,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let princ_type = EConstr.of_constr princ_type in
+    let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
     *)
@@ -717,7 +719,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
+	  Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar ids));
 	  thin ids
 	]
       else
@@ -756,10 +758,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
+	(Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -939,7 +941,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
+		      Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid]))]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -972,18 +974,18 @@ let functional_inversion kn hid fconst f_correct : tactic =
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term type_of_h with
-      | App(eq,args) when eq_constr eq (make_eq ())  ->
+      | App(eq,args) when Term.eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
-	      | App(f,f_args),_ when eq_constr f fconst ->
+	      | App(f,f_args),_ when Term.eq_constr f fconst ->
 		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-	      |_,App(f,f_args) when eq_constr f fconst ->
+	      |_,App(f,f_args) when Term.eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
+	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(f_correct,(Array.to_list f_args)@[res;mkVar hid]))]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
@@ -1024,7 +1026,7 @@ let invfun qhyp f g =
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
 	     match kind_of_term hyp_typ with
-	       | App(eq,args) when eq_constr eq (make_eq ()) ->
+	       | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
 		   begin
 		     let f1,_ = decompose_app args.(1) in
 		     try
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 222c0c804..3688b8c15 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -32,7 +32,7 @@ module RelDecl = Context.Rel.Declaration
 
 (** {2 Useful operations on constr and glob_constr} *)
 
-let rec popn i c = if i<=0 then c else pop (EConstr.of_constr (popn (i-1) c))
+let rec popn i c = if i<=0 then c else EConstr.of_constr (pop (popn (i-1) c))
 
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
@@ -979,19 +979,20 @@ let funify_branches relinfo nfuns branch =
 
 
 let relprinctype_to_funprinctype relprinctype nfuns =
-  let relinfo = compute_elim_sig relprinctype in
+  let relprinctype = EConstr.of_constr relprinctype in
+  let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in
   assert (not relinfo.farg_in_concl);
   assert (relinfo.indarg_in_concl);
   (* first remove indarg and indarg_in_concl *)
   let relinfo_noindarg = { relinfo with
     indarg_in_concl = false; indarg = None;
-    concl = remove_last_arg (pop (EConstr.of_constr relinfo.concl)); } in
+    concl = EConstr.of_constr (remove_last_arg (pop relinfo.concl)); } in
   (* the nfuns last induction arguments are functional ones: remove them *)
   let relinfo_argsok = { relinfo_noindarg with
     nargs = relinfo_noindarg.nargs - nfuns;
     (* args is in reverse order, so remove fst *)
     args = remove_n_fst_list nfuns relinfo_noindarg.args;
-    concl = popn nfuns relinfo_noindarg.concl
+    concl = popn nfuns relinfo_noindarg.concl;
   } in
   let new_branches =
     List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b2c93a754..d5ee42af8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -286,7 +286,7 @@ let tclUSER tac is_mes l g =
 
 let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
   if is_mes
-  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
+  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (delayed_force well_founded_ltof))) gl)
   else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
 
 
@@ -465,7 +465,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
       end
     | App _ -> 
       let f,args = decompose_app expr_info.info in 
-      if eq_constr f (expr_info.f_constr) 
+      if Term.eq_constr f (expr_info.f_constr) 
       then jinfo.app_reC (f,args) expr_info continuation_tac expr_info 
       else
       begin
@@ -517,21 +517,21 @@ let rec prove_lt hyple g =
       let h =
 	List.find (fun id ->
           match decompose_app (pf_unsafe_type_of g (EConstr.mkVar id)) with
-            | _, t::_ -> eq_constr t varx
+            | _, t::_ -> Term.eq_constr t varx
             | _ -> false
 	) hyple
       in
       let y =
 	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (EConstr.mkVar h))))) in
       observe_tclTHENLIST (str "prove_lt1")[
-	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
+	Proofview.V82.of_tactic (apply (EConstr.of_constr (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))));
 	observe_tac (str "prove_lt") (prove_lt hyple)
       ]
     with Not_found -> 
       (
 	(
 	  observe_tclTHENLIST (str "prove_lt2")[
-	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
+	    Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force lt_S_n)));
 	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
       )
@@ -549,15 +549,15 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
       observe_tclTHENLIST (str "destruct_bounds_aux1")[
-	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
+	Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr s_max]));
 	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
             Proofview.V82.tactic begin
 	    observe_tac (str "destruct_bounds_aux") 
-	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
+	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id)))
 		 [
 		   observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id);
-			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
+			       Proofview.V82.of_tactic (simplest_elim(EConstr.of_constr (mkApp(delayed_force lt_n_O,[|s_max|]))));
 			       Proofview.V82.of_tactic default_full_auto];
 		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
 		     observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
@@ -588,7 +588,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	  ] g
       | (_,v_bound)::l -> 
       observe_tclTHENLIST (str "destruct_bounds_aux3")[
-	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
+	Proofview.V82.of_tactic (simplest_elim (EConstr.mkVar v_bound));
 	Proofview.V82.of_tactic (clear [v_bound]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
@@ -597,7 +597,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	       (fun p ->  
 		 observe_tclTHENLIST (str "destruct_bounds_aux4")[
 		   Proofview.V82.of_tactic (simplest_elim 
-		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
+		     (EConstr.of_constr (mkApp(delayed_force max_constr, [| bound; mkVar p|]))));
 		   tclDO 3 (Proofview.V82.of_tactic intro);
 		   onNLastHypsId 3 (fun lids -> 
 		     match lids with
@@ -622,7 +622,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
       observe_tclTHENLIST (str "terminate_app1")[
 	continuation_tac infos;
 	observe_tac (str "first split") 
-	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+	  (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
 	observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
@@ -633,7 +633,7 @@ let terminate_others _ expr_info continuation_tac infos =
     observe_tclTHENLIST (str "terminate_others")[
 	    continuation_tac infos;
       observe_tac (str "first split") 
-	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+	(Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
       observe_tac (str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
@@ -657,7 +657,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.type_of (pf_env gl) (project gl) (EConstr.of_constr 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 =
@@ -687,16 +687,18 @@ let mkDestructEq :
   let type_of_expr = pf_unsafe_type_of g (EConstr.of_constr expr) in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
+  let new_hyps = List.map EConstr.of_constr new_hyps in
     pf_typel new_hyps (fun _ ->
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
-          redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
+          let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
+          Sigma (EConstr.of_constr c, sigma, p)
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
-      Proofview.V82.of_tactic (simplest_case expr)]), to_revert
+      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr expr))]), to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -742,7 +744,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	then
 	  observe_tclTHENLIST (str "terminate_app_rec1")[ 
 	    observe_tac (str "first split")
-	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+	      (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
 	    observe_tac (str "destruct_bounds (3)")
 	      (destruct_bounds new_infos)
 	  ]
@@ -751,7 +753,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
       ]    
     with Not_found -> 
       observe_tac (str "terminate_app_rec not found") (tclTHENS
-	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
+	(Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr (mkApp(mkVar expr_info.ih,Array.of_list args)))))
 	[		
 	  observe_tclTHENLIST (str "terminate_app_rec2")[
 	    Proofview.V82.of_tactic (intro_using rec_res_id);
@@ -772,7 +774,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 		       then
 			 observe_tclTHENLIST (str "terminate_app_rec4")[ 
 			   observe_tac (str "first split") 
-			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+			     (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
 			   observe_tac (str "destruct_bounds (2)") 
 			     (destruct_bounds new_infos)
 			 ]
@@ -785,7 +787,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	  ];
 	  observe_tac (str "proving decreasing") (
 	    tclTHENS (* proof of args < formal args *)
-	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
+	      (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force expr_info.acc_inv))))
 	      [ 
 		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
 		observe_tclTHENLIST (str "terminate_app_rec5")
@@ -833,7 +835,7 @@ let rec prove_le g =
   in 
   tclFIRST[
     Proofview.V82.of_tactic assumption;
-    Proofview.V82.of_tactic (apply (delayed_force le_n));
+    Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_n)));
     begin
       try
 	let matching_fun = 
@@ -846,7 +848,7 @@ let rec prove_le g =
 	  List.hd (List.tl args)
 	in 
 	observe_tclTHENLIST (str "prove_le")[
-	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
+	  Proofview.V82.of_tactic (apply(EConstr.of_constr (mkApp(le_trans (),[|x;y;z;mkVar h|]))));
 	  observe_tac (str "prove_le (rec)") (prove_le)
 	] 
       with Not_found -> tclFAIL 0 (mt())
@@ -876,7 +878,7 @@ let rec make_rewrite_list expr_info max = function
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
-	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
+	 Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_n_Sm)));
 	 observe_tac (str "prove_le(2)") prove_le
        ]
       ] )
@@ -916,7 +918,7 @@ let make_rewrite expr_info l hp max =
 	    ]))
        ;
 	 observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *)
-	 Proofview.V82.of_tactic (apply (delayed_force le_lt_SS));
+	 Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS)));
 	 observe_tac (str "prove_le (3)") prove_le
 	 ]
        ])  
@@ -928,7 +930,7 @@ let rec compute_max rew_tac max l =
     | (_,p,_)::l -> 
       observe_tclTHENLIST (str "compute_max")[
 	Proofview.V82.of_tactic (simplest_elim 
-	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
+	  (EConstr.of_constr (mkApp(delayed_force max_constr, [| max; mkVar p|]))));
 	tclDO 3 (Proofview.V82.of_tactic intro);
 	onNLastHypsId 3 (fun lids -> 
 	  match lids with
@@ -947,7 +949,7 @@ let rec destruct_hex expr_info acc l =
       end
     | (v,hex)::l -> 
       observe_tclTHENLIST (str "destruct_hex")[
-	Proofview.V82.of_tactic (simplest_case (mkVar hex));
+	Proofview.V82.of_tactic (simplest_case (EConstr.mkVar hex));
 	Proofview.V82.of_tactic (clear [hex]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
@@ -995,13 +997,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info =
       if expr_info.is_final && expr_info.is_main_branch 
       then 
 	observe_tclTHENLIST (str "equation_app_rec")
-	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+	  [ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
 	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
 	  ]
       else 
 	observe_tclTHENLIST (str "equation_app_rec1")[
-  	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+  	  Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
 	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
 	]
   end
@@ -1086,9 +1088,9 @@ let termination_proof_header is_mes input_type ids args_id relation
 	      (str "first assert")
 	      (Proofview.V82.of_tactic (assert_before
 		 (Name wf_rec_arg)
-		 (mkApp (delayed_force acc_rel,
+		 (EConstr.of_constr (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
-		 )
+		 ))
 	      ))
 	   )
 	   [
@@ -1098,7 +1100,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		  (str "second assert")
 		  (Proofview.V82.of_tactic (assert_before
 		     (Name wf_thm)
-		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		     (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
 		  ))
 	       )
 	       [
@@ -1107,7 +1109,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		 (* this gives the accessibility argument *)
 		 observe_tac
 		   (str "apply wf_thm")
-		   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
+		   (Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))))
 		   )
 	       ]
 	     ;
@@ -1116,7 +1118,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
-			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
+			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
 		observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
@@ -1214,7 +1216,7 @@ let build_and_l l =
       | Prod(_,_,t') -> is_well_founded t'
       | App(_,_) -> 
 	let (f,_) = decompose_app t in 
-	eq_constr f (well_founded ())
+	Term.eq_constr f (well_founded ())
       | _ -> 
 	false
   in
@@ -1231,7 +1233,7 @@ let build_and_l l =
 	let c,tac,nb = f pl in
 	mk_and p1 c,
 	tclTHENS
-	  (Proofview.V82.of_tactic (apply (constr_of_global conj_constr)))
+	  (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr))))
 	  [tclIDTAC;
 	   tac
 	  ],nb+1
@@ -1297,6 +1299,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
     ref_ := Some lemma ;
+    let lemma = EConstr.of_constr lemma in
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
@@ -1323,7 +1326,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	     ] gls)
       (fun g ->
 	 match kind_of_term (pf_concl g) with
-	   | App(f,_) when eq_constr f (well_founded ()) ->
+	   | App(f,_) when Term.eq_constr f (well_founded ()) ->
 	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
 	       incr h_num;
@@ -1332,11 +1335,11 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		    tclCOMPLETE(
 		      tclFIRST[
 			tclTHEN
-			  (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
+			  (Proofview.V82.of_tactic (eapply_with_bindings (EConstr.mkVar (List.nth !lid !h_num), NoBindings)))
 			  (Proofview.V82.of_tactic e_assumption);
 		      Eauto.eauto_with_bases
 			(true,5)
-			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
 			[Hints.Hint_db.empty empty_transparent_state false]
 		      ]
 		    )
@@ -1366,7 +1369,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	 	     (fun c ->
 	 		Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST 
 	 		  [intros;
-	 		   Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
+	 		   Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*);
 	 		   Tacticals.New.tclCOMPLETE Auto.default_auto
 	 		  ])
 	 	     )
@@ -1428,8 +1431,8 @@ let start_equation (f:global_reference) (term_f:global_reference)
     h_intros x;
     Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
     observe_tac (str "simplest_case")
-      (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
-                             Array.of_list (List.map mkVar x)))));
+      (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (terminate_constr,
+                             Array.of_list (List.map mkVar x))))));
     observe_tac (str "prove_eq") (cont_tactic x)]) g;;
 
 let (com_eqn : int -> Id.t ->