Tactics API using EConstr.

10 files changed, 93 insertions, 63 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 28ff6df838..20d9640fc4 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -27,7 +27,7 @@ TACTIC EXTEND reflexivity
 END
 
 TACTIC EXTEND exact
-  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND assumption
@@ -39,35 +39,35 @@ TACTIC EXTEND etransitivity
 END
 
 TACTIC EXTEND cut
-  [ "cut" constr(c) ] -> [ Tactics.cut c ]
+  [ "cut" constr(c) ] -> [ Tactics.cut (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
+  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND vm_cast_no_check
-  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
+  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND native_cast_no_check
-  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
+  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND casetype
-  [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
+  [ "casetype" constr(c) ] -> [ Tactics.case_type (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND elimtype
-  [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
+  [ "elimtype" constr(c) ] -> [ Tactics.elim_type (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND lapply
-  [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
+  [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply (EConstr.of_constr c) ]
 END
 
 TACTIC EXTEND transitivity
-  [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
+  [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some (EConstr.of_constr c)) ]
 END
 
 (** Left *)
@@ -297,7 +297,7 @@ END
 (* Generalize dependent *)
 
 TACTIC EXTEND generalize_dependent
-  [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
+  [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep (EConstr.of_constr c) ]
 END
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 3e7cf5d13b..c39b1a0e94 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -118,7 +118,7 @@ END
 
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
+  discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
 
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None) with_evars c
@@ -150,7 +150,7 @@ END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  injection_main false { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
+  injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -301,6 +301,7 @@ let project_hint pri l2r r =
   let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let t =
     Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in
+  let t = EConstr.Unsafe.to_constr t in
   let sign,ccl = decompose_prod_assum t in
   let (a,b) = match snd (decompose_app ccl) with
     | [a;b] -> (a,b)
@@ -475,6 +476,7 @@ let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l"
 let step left x tac =
   let l =
     List.map (fun lem ->
+      let lem = EConstr.of_constr lem in
       Tacticals.New.tclTHENLAST
         (apply_with_bindings (lem, ImplicitBindings [x]))
         tac)
@@ -510,13 +512,13 @@ let add_transitivity_lemma left lem =
 (* Vernacular syntax *)
 
 TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ]
-| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ]
+| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ]
+| ["stepl" constr(c) ] -> [ step true (EConstr.of_constr c) (Proofview.tclUNIT ()) ]
 END
 
 TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ]
-| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ]
+| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ]
+| ["stepr" constr(c) ] -> [ step false (EConstr.of_constr c) (Proofview.tclUNIT ()) ]
 END
 
 VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF
@@ -660,7 +662,7 @@ let hResolve id c occ t =
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma (EConstr.of_constr t_constr) in
   let tac =
-    (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
+    (change_concl (EConstr.of_constr (mkLetIn (Anonymous,t_constr,t_constr_type,concl))))
   in
   Sigma.Unsafe.of_pair (tac, sigma)
   end }
@@ -694,7 +696,7 @@ let hget_evar n =
   if n <= 0 then error "Incorrect existential variable index.";
   let ev = List.nth evl (n-1) in
   let ev_type = existential_type sigma ev in
-  change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
+  change_concl (EConstr.of_constr (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)))
   end }
 
 TACTIC EXTEND hget_evar
@@ -736,15 +738,16 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in
        Tacticals.New.tclTHENLIST
-         [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
+         [Tactics.generalize [EConstr.of_constr (mkApp(delayed_force refl_equal, [| type_of_a; a|]))];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
             let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], EConstr.of_constr a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in
+            let c = EConstr.of_constr c in
 	    change_concl c
           end };
-	  simplest_case a]
+	  simplest_case (EConstr.of_constr a)]
   end }
 
 
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 82ba63871e..c6395d7e28 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -48,7 +48,11 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true
   } in
-  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
+  let map c = { delayed = fun env sigma ->
+    let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in
+    Sigma.Sigma (EConstr.of_constr c, sigma, p)
+  } in
+  List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
 
@@ -153,7 +157,7 @@ TACTIC EXTEND autounfoldify
 END
 
 TACTIC EXTEND unify
-| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ]
+| ["unify" constr(x) constr(y) ] -> [ Tactics.unify (EConstr.of_constr x) (EConstr.of_constr y) ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
     let table = try Some (Hints.searchtable_map base) with Not_found -> None in
     match table with
@@ -162,13 +166,13 @@ TACTIC EXTEND unify
       Tacticals.New.tclZEROMSG msg
     | Some t ->
       let state = Hints.Hint_db.transparent_state t in
-      Tactics.unify ~state x y
+      Tactics.unify ~state (EConstr.of_constr x) (EConstr.of_constr y)
   ]
 END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check (EConstr.of_constr x) Term.DEFAULTcast ]
 END
 
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index b1c4f58eb8..bae5a516c7 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -265,7 +265,7 @@ TACTIC EXTEND setoid_reflexivity
 END
 
 TACTIC EXTEND setoid_transitivity
-  [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
+  [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some (EConstr.of_constr t)) ]
 | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
 END
 
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index 6230fa0606..934830f4db 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -1158,11 +1158,12 @@ module Make
   let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
   let strip_prod_binders_constr n ty =
+    let ty = EConstr.Unsafe.to_constr ty in
     let rec strip_ty acc n ty =
-      if n=0 then (List.rev acc, ty) else
+      if n=0 then (List.rev acc, EConstr.of_constr ty) else
         match Term.kind_of_term ty with
             Term.Prod(na,a,b) ->
-              strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+              strip_ty (([Loc.ghost,na],EConstr.of_constr a)::acc) (n-1) b
           | _ -> error "Cannot translate fix tactic: not enough products" in
     strip_ty [] n ty
 
@@ -1170,9 +1171,9 @@ module Make
     let prtac n (t:atomic_tactic_expr) =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
-        pr_constr = pr_constr_env env Evd.empty;
+        pr_constr = (fun c -> pr_constr_env env Evd.empty (EConstr.Unsafe.to_constr c));
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_lconstr = pr_lconstr_env env Evd.empty;
+        pr_lconstr = (fun c -> pr_lconstr_env env Evd.empty (EConstr.Unsafe.to_constr c));
         pr_pattern = pr_constr_pattern_env env Evd.empty;
         pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
         pr_constant = pr_evaluable_reference_env env;
@@ -1284,7 +1285,7 @@ let () =
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed c)))));
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
@@ -1317,15 +1318,15 @@ let () =
   Genprint.register_print0 wit_bindings
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+    (fun it -> pr_bindings_no_with (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it)));
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
+    (fun it -> pr_with_bindings (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it)));
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it));
+    (fun it -> pr_destruction_arg (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (run_delayed_destruction_arg it));
   Genprint.register_print0 Stdarg.wit_int int int int;
   Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
   Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 52cf1ff357..ef2ab09176 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -97,8 +97,8 @@ let new_cstr_evar (evd,cstrs) env t =
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd (EConstr.of_constr t) in
   let evd' = Sigma.to_evar_map evd' in
-  let ev, _ = destEvar t in
-    (evd', Evar.Set.add ev cstrs), t
+  let ev, _ = EConstr.destEvar evd' t in
+    (evd', Evar.Set.add ev cstrs), EConstr.Unsafe.to_constr t
 
 (** Building or looking up instances. *)
 let e_new_cstr_evar env evars t =
@@ -363,6 +363,7 @@ end) = struct
 	   let env' = Environ.push_rel_context rels env in
 	   let sigma = Sigma.Unsafe.of_evar_map sigma in
 	   let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+	   let evar = EConstr.Unsafe.to_constr evar in
 	   let evars = Sigma.to_evar_map evars in
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
@@ -774,7 +775,7 @@ let poly_subrelation sort =
   if sort then PropGlobal.subrelation else TypeGlobal.subrelation
 
 let resolve_subrelation env avoid car rel sort prf rel' res =
-  if eq_constr rel rel' then res
+  if Termops.eq_constr (fst res.rew_evars) (EConstr.of_constr rel) (EConstr.of_constr rel') then res
   else
     let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
     let evars, subrel = new_cstr_evar evars env app in
@@ -872,7 +873,7 @@ let apply_rule unify loccs : int pure_strategy =
         | Some rew ->
 	  let occ = succ occ in
 	    if not (is_occ occ) then (occ, Fail)
-	    else if eq_constr t rew.rew_to then (occ, Identity)
+	    else if Termops.eq_constr (fst rew.rew_evars) (EConstr.of_constr t) (EConstr.of_constr rew.rew_to) then (occ, Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
               let rel, prf = get_rew_prf res in
@@ -1111,7 +1112,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       | Prod (n, dom, codom) ->
 	  let lam = mkLambda (n, dom, codom) in
 	  let (evars', app), unfold = 
-	    if eq_constr ty mkProp then
+	    if eq_constr (fst evars) (EConstr.of_constr ty) EConstr.mkProp then
 	      (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
 	    else 
 	      let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
@@ -1409,7 +1410,7 @@ module Strategies =
           let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
 	  let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma (EConstr.of_constr t) in
 	  let evars' = Sigma.to_evar_map sigma in
-	    if eq_constr t' t then
+	    if Termops.eq_constr evars' (EConstr.of_constr t') (EConstr.of_constr t) then
 	      state, Identity
 	    else
 	      state, Success { rew_car = ty; rew_from = t; rew_to = t';
@@ -1553,14 +1554,15 @@ let assert_replacing id newt tac =
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Refine.refine ~unsafe:false { run = begin fun sigma ->
+      let open EConstr in
       let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma (EConstr.of_constr concl) in
       let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in
       let map d =
         let n = NamedDecl.get_id d in
-        if Id.equal n id then ev' else mkVar n
+        if Id.equal n id then ev' else EConstr.mkVar n
       in
-      let (e, _) = destEvar ev in
-      Sigma (EConstr.of_constr (mkEvar (e, Array.map_of_list map nc)), sigma, p +> q)
+      let (e, _) = EConstr.destEvar (Sigma.to_evar_map sigma) ev in
+      Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
     end }
   end } in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1596,16 +1598,18 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             convert_hyp_no_check (LocalAssum (id, newt)) <*>
             beta_hyp id
 	| None, Some p ->
+            let p = EConstr.of_constr p in
             Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter { enter = begin fun gl ->
             let env = Proofview.Goal.env gl in
             let make = { run = begin fun sigma ->
               let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in
-              Sigma (EConstr.of_constr (mkApp (p, [| ev |])), sigma, q)
+              Sigma (EConstr.mkApp (p, [| ev |]), sigma, q)
             end } in
             Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end }
 	| None, None ->
+            let newt = EConstr.of_constr newt in
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
@@ -2168,7 +2172,7 @@ let setoid_reflexivity =
      tac_open (poly_proof PropGlobal.get_reflexive_proof
 			  TypeGlobal.get_reflexive_proof
 			  env evm car rel)
-	      (fun c -> tclCOMPLETE (apply c)))
+	      (fun c -> tclCOMPLETE (apply (EConstr.of_constr c))))
     (reflexivity_red true)
 
 let setoid_symmetry =
@@ -2177,7 +2181,7 @@ let setoid_symmetry =
       tac_open
 	(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
 	   env evm car rel)
-	(fun c -> apply c))
+	(fun c -> apply (EConstr.of_constr c)))
     (symmetry_red true)
     
 let setoid_transitivity c =
@@ -2186,8 +2190,8 @@ let setoid_transitivity c =
       tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
 	   env evm car rel)
 	(fun proof -> match c with
-	| None -> eapply proof
-	| Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
+	| None -> eapply (EConstr.of_constr proof)
+	| Some c -> apply_with_bindings (EConstr.of_constr proof,ImplicitBindings [ c ])))
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
@@ -2204,10 +2208,11 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
+  let new_hyp = EConstr.of_constr new_hyp in
    Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
-      (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
+      (tclTHENLIST [ intros; setoid_symmetry; apply (EConstr.mkVar id); Tactics.assumption ]))
       gl)
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index 35c4483513..bf56eec10e 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -105,7 +105,7 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic
 
 val setoid_reflexivity : unit Proofview.tactic
 
-val setoid_transitivity : constr option -> unit Proofview.tactic
+val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic
 
 
 val apply_strategy :
diff --git a/ltac/tacexpr.mli b/ltac/tacexpr.mli
index 9c25a16457..b8d2d42b7d 100644
--- a/ltac/tacexpr.mli
+++ b/ltac/tacexpr.mli
@@ -120,9 +120,9 @@ type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr *
 type 'a delayed_open = 'a Tactypes.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
-type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
 
-type delayed_open_constr = Term.constr delayed_open
+type delayed_open_constr = EConstr.constr delayed_open
 
 type intro_pattern = delayed_open_constr intro_pattern_expr located
 type intro_patterns = delayed_open_constr intro_pattern_expr located list
@@ -354,7 +354,7 @@ type raw_tactic_arg =
 
 (** Interpreted tactics *)
 
-type t_trm = Term.constr
+type t_trm = EConstr.constr
 type t_pat = constr_pattern
 type t_cst = evaluable_global_reference
 type t_ref = ltac_constant located
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 142f061b5a..5535656391 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -746,11 +746,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
 
 let interp_constr_with_occurrences_and_name_as_list =
   interp_constr_in_compound_list
-    (fun c -> ((AllOccurrences,c),Anonymous))
+    (fun c -> ((AllOccurrences,EConstr.of_constr c),Anonymous))
     (function ((occs,c),Anonymous) when occs == AllOccurrences -> c
       | _ -> raise Not_found)
     (fun ist env sigma (occ_c,na) ->
       let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
+      let c_interp = (fst c_interp, EConstr.of_constr (snd c_interp)) in
       sigma, (c_interp,
        interp_name ist env sigma na))
 
@@ -853,7 +854,7 @@ let rec message_of_value v =
     Ftactic.return (int (out_gen (topwit wit_int) v))
   else if has_type v (topwit wit_intro_pattern) then
     let p = out_gen (topwit wit_intro_pattern) v in
-    let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in
+    let print env sigma c = pr_constr_env env sigma (EConstr.Unsafe.to_constr (fst (Tactics.run_delayed env Evd.empty c))) in
     Ftactic.nf_enter { enter = begin fun gl ->
       Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
     end }
@@ -917,6 +918,7 @@ and interp_intro_pattern_action ist env sigma = function
       let c = { delayed = fun env sigma ->
         let sigma = Sigma.to_evar_map sigma in
         let (sigma, c) = interp_open_constr ist env sigma c in
+        let c = EConstr.of_constr c in
         Sigma.Unsafe.of_pair (c, sigma)
       } in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
@@ -1002,6 +1004,8 @@ let interp_bindings ist env sigma = function
 let interp_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
   let sigma, c = interp_open_constr ist env sigma c in
+  let c = EConstr.of_constr c in
+  let bl = Miscops.map_bindings EConstr.of_constr bl in
   sigma, (c,bl)
 
 let interp_open_constr_with_bindings ist env sigma (c,bl) =
@@ -1021,6 +1025,7 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let f = { delayed = fun env sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in
+    let c = Miscops.map_with_bindings EConstr.of_constr c in
     Sigma.Unsafe.of_pair (c, sigma)
   } in
     (loc,f)
@@ -1044,7 +1049,7 @@ let interp_destruction_arg ist gl arg =
         then keep,ElimOnIdent (loc,id')
         else
           (keep, ElimOnConstr { delayed = begin fun env sigma ->
-          try Sigma.here (constr_of_id env id', NoBindings) sigma
+          try Sigma.here (EConstr.of_constr (constr_of_id env id'), NoBindings) sigma
           with Not_found ->
             user_err ~loc  ~hdr:"interp_destruction_arg" (
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
@@ -1066,7 +1071,7 @@ let interp_destruction_arg ist gl arg =
           keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
         else match Value.to_constr v with
         | None -> error ()
-        | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) }
+        | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) }
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
@@ -1076,6 +1081,7 @@ let interp_destruction_arg ist gl arg =
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
+            let c = EConstr.of_constr c in
             Sigma.Unsafe.of_pair ((c,NoBindings), sigma)
           } in
           keep,ElimOnConstr f
@@ -1701,7 +1707,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,n,c) =
           let (sigma,c_interp) = interp_type ist env sigma c in
-	  sigma , (interp_ident ist env sigma id,n,c_interp) in
+	  sigma , (interp_ident ist env sigma id,n,EConstr.of_constr c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
@@ -1716,7 +1722,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = interp_type ist env sigma c in
-	  sigma , (interp_ident ist env sigma id,c_interp) in
+	  sigma , (interp_ident ist env sigma id,EConstr.of_constr c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
@@ -1731,6 +1737,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,c) = 
           (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
         in
+        let c = EConstr.of_constr c in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (Option.map (interp_tactic ist)) t in
         Tacticals.New.tclWITHHOLES false
@@ -1758,6 +1765,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         if Locusops.is_nowhere clp then
         (* We try to fully-typecheck the term *)
           let (sigma,c_interp) = interp_constr ist env sigma c in
+          let c_interp = EConstr.of_constr c_interp in
           let let_tac b na c cl eqpat =
             let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
@@ -1776,11 +1784,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
             Tactics.letin_pat_tac with_eq na c cl
           in
           let (sigma',c) = interp_pure_open_constr ist env sigma c in
+          let c = EConstr.of_constr c in
           name_atomic ~env
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
                (let_pat_tac b (interp_name ist env sigma na)
-                  ((sigma,sigma'),EConstr.of_constr c) clp eqpat) sigma')
+                  ((sigma,sigma'),c) clp eqpat) sigma')
       end }
 
   (* Derived basic tactics *)
@@ -1845,6 +1854,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             then interp_type ist (pf_env gl) sigma c
             else interp_constr ist (pf_env gl) sigma c
           in
+          let c = EConstr.of_constr c in
           Sigma.Unsafe.of_pair (c, sigma)
         end } in
         Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
@@ -1868,6 +1878,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             try
               let sigma = Sigma.to_evar_map sigma in
               let (sigma, c) = interp_constr ist env sigma c in
+              let c = EConstr.of_constr c in
               Sigma.Unsafe.of_pair (c, sigma)
             with e when to_catch e (* Hack *) ->
               user_err  (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
@@ -1884,6 +1895,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in
+            let c = Miscops.map_with_bindings EConstr.of_constr c in
             Sigma.Unsafe.of_pair (c, sigma)
           } in
 	  (b,m,keep,f)) l in
@@ -1906,6 +1918,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | None -> sigma , None
           | Some c ->
               let (sigma,c_interp) = interp_constr ist env sigma c in
+              let c_interp = EConstr.of_constr c_interp in
               sigma , Some c_interp
         in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
@@ -1932,6 +1945,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c_interp) = interp_constr ist env sigma c in
+        let c_interp = EConstr.of_constr c_interp in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let hyps = interp_hyp_list ist env sigma idl in
         let tac = name_atomic ~env
@@ -2041,6 +2055,7 @@ end }
 
 let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma ->
   let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in
+  let bl = Miscops.map_bindings EConstr.of_constr bl in
   Sigma.Unsafe.of_pair (bl, sigma)
   }
 
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 11996af731..e3f5342ded 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -161,8 +161,9 @@ let flatten_contravariant_conj _ ist =
   | Some (_,args) ->
     let args = List.map EConstr.Unsafe.to_constr args in
     let newtyp = List.fold_right mkArrow args c in
+    let newtyp = EConstr.of_constr newtyp in
     let intros = tclMAP (fun _ -> intro) args in
-    let by = tclTHENLIST [intros; apply hyp; split; assumption] in
+    let by = tclTHENLIST [intros; apply (EConstr.of_constr hyp); split; assumption] in
     tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)]
   | _ -> fail
 
@@ -186,17 +187,17 @@ let flatten_contravariant_disj _ ist =
   let typ = assoc_var "X1" ist in
   let typ = EConstr.of_constr typ in
   let c = assoc_var "X2" ist in
+  let c = EConstr.of_constr c in
   let hyp = assoc_var "id" ist in
   match match_with_disjunction sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode
           typ with
   | Some (_,args) ->
-      let args = List.map EConstr.Unsafe.to_constr args in
       let map i arg =
-        let typ = mkArrow arg c in
+        let typ = EConstr.mkArrow arg c in
         let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in
-        let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
+        let by = tclTHENLIST [intro; apply (EConstr.of_constr hyp); ci; assumption] in
         assert_ ~by typ
       in
       let tacs = List.mapi map args in
@@ -231,6 +232,7 @@ let apply_nnpp _ ist =
     (Proofview.tclUNIT ())
     begin fun () -> try
       let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
+      let nnpp = EConstr.of_constr nnpp in
       apply nnpp
     with Not_found -> tclFAIL 0 (Pp.mt ())
     end