Elim API using EConstr.

4 files changed, 15 insertions, 12 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index e641f970aa..ef848c2e13 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -10,6 +10,7 @@ open Util
 open Names
 open Term
 open Termops
+open EConstr
 open Inductiveops
 open Hipattern
 open Tacmach.New
@@ -55,7 +56,7 @@ Another example :
 *)
 
 let elimHypThen tac id =
-  elimination_then tac (EConstr.mkVar id)
+  elimination_then tac (mkVar id)
 
 let rec general_decompose_on_hyp recognizer =
   ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
@@ -77,7 +78,6 @@ let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
-  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let sigma = project gl in
@@ -105,17 +105,17 @@ let head_in indl t gl =
 let decompose_these c l =
   Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun sigma (_,t) -> head_in indl (EConstr.of_constr t) gl) c
+  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
   end }
 
 let decompose_and c =
   general_decompose
-    (fun sigma (_,t) -> is_record sigma (EConstr.of_constr t))
+    (fun sigma (_,t) -> is_record sigma t)
     c
 
 let decompose_or c =
   general_decompose
-    (fun sigma (_,t) -> is_disjunction sigma (EConstr.of_constr t))
+    (fun sigma (_,t) -> is_disjunction sigma t)
     c
 
 let h_decompose l c = decompose_these c l
@@ -127,7 +127,7 @@ let h_decompose_and = decompose_and
 (* The tactic Double performs a double induction *)
 
 let simple_elimination c =
-  elimination_then (fun _ -> tclIDTAC) (EConstr.of_constr c)
+  elimination_then (fun _ -> tclIDTAC) c
 
 let induction_trailer abs_i abs_j bargs =
   tclTHEN
@@ -135,8 +135,9 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.nf_enter { enter = begin fun gl ->
-	  let idty = pf_unsafe_type_of gl (EConstr.mkVar id) in
-	  let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
+	  let idty = pf_unsafe_type_of gl (mkVar id) in
+	  let idty = EConstr.of_constr idty in
+	  let fvty = global_vars (pf_env gl) (project gl) idty in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
           in
@@ -168,7 +169,7 @@ let double_ind h1 h2 =
      (onLastHypId
        	(fun id ->
            elimination_then
-             (introElimAssumsThen (induction_trailer abs_i abs_j)) (EConstr.mkVar id))))
+             (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
   end }
 
 let h_double_induction = double_ind
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 29c4414636..dc1af79ba0 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Tacticals
 open Misctypes
 open Tactypes
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e15ee149d1..e440f1dc51 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -128,7 +128,7 @@ let onClauseLR tac cl gls =
   tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls
 
 let ifOnHyp pred tac1 tac2 id gl =
-  if pred (id,pf_get_hyp_typ gl id) then
+  if pred (id,EConstr.of_constr (pf_get_hyp_typ gl id)) then
     tac1 id gl
   else
     tac2 id gl
@@ -583,6 +583,7 @@ module New = struct
   let ifOnHyp pred tac1 tac2 id =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
+    let typ = EConstr.of_constr typ in
     if pred (id,typ) then
       tac1 id
     else
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2c3e512806..e4f110722b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -76,7 +76,7 @@ val nLastDecls  : int -> goal sigma -> Context.Named.t
 
 val afterHyp    : Id.t -> goal sigma -> Context.Named.t
 
-val ifOnHyp     : (Id.t * types -> bool) ->
+val ifOnHyp     : (Id.t * EConstr.types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
@@ -230,7 +230,7 @@ module New : sig
 
   val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
 
-  val ifOnHyp     : (identifier * types -> bool) ->
+  val ifOnHyp     : (identifier * EConstr.types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
     identifier -> unit Proofview.tactic