Removing Tacmach compatibility layer in Inv.

10 files changed, 39 insertions, 24 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 943974489..fcba8119d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -271,4 +271,10 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_betadeltaiota gl (pf_get_type_of gl t)
 
+  let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t
+
+  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+
+  let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t
+
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index bf0ce04a1..d122b0941 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -148,5 +148,13 @@ module New : sig
 
   val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
   val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types
+
   val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
+
+  val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
+
+  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+
+  val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
+
 end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b16f956d0..de2acaf1d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1461,12 +1461,12 @@ let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL
 let try_rewrite tac =
   Proofview.tclORELSE tac begin function
     | ConstrMatching.PatternMatchingFailure ->
-	Tactics.New.tclZEROMSG (str "Not a primitive equality here.")
+	Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
     | e when catchable_exception e ->
-	Tactics.New.tclZEROMSG
+	Tacticals.New.tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
     | NothingToRewrite ->
-	Tactics.New.tclZEROMSG
+	Tacticals.New.tclZEROMSG
           (strbrk "Nothing to rewrite.")
     | e -> Proofview.tclZERO e
   end
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index cc3c4c297..6cc0af2c6 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -421,10 +421,10 @@ let find_this_eq_data_decompose gl eqn =
 open Tacmach
 
 let match_eq_nf gls eqn eq_pat =
-  match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
+  match Id.Map.bindings (Tacmach.New.pf_matches gls (Lazy.force eq_pat) eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
+	(t,Tacmach.New.pf_whd_betadeltaiota gls x,Tacmach.New.pf_whd_betadeltaiota gls y)
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index f8a4d35a8..fc87fc9ed 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -147,7 +147,7 @@ val match_eqdec : constr -> bool * constr * constr * constr * constr
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 open Proof_type
 open Tacmach
-val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr)
+val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7a344eeeb..e2129ce53 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -20,7 +20,7 @@ open Environ
 open Inductiveops
 open Printer
 open Retyping
-open Tacmach
+open Tacmach.New
 open Clenv
 open Tacticals.New
 open Tactics
@@ -192,7 +192,7 @@ let dependent_hyps id idlist gl =
     | [] -> []
     | (id1,_,_)::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
-	let d = Tacmach.New.pf_get_hyp id1 gl in
+	let d = pf_get_hyp id1 gl in
 	if occur_var_in_decl (Global.env()) id d
         then d :: dep_rec l
         else dep_rec l
@@ -307,10 +307,10 @@ let projectAndApply thin id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Proofview.Goal.enter begin fun gl ->
-    let (t,t1,t2) =
-      Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) gl
-    in
+    Proofview.Goal.raw_enter begin fun gl ->
+    (** We only look at the type of hypothesis "id" *)
+    let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
+    let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
     match (kind_of_term t1, kind_of_term t2) with
     | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1
     | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2
@@ -461,8 +461,8 @@ let raw_inversion inv_kind id status names =
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
-    let reduce_to_atomic_ind = Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind gl in
-    let type_of = Tacmach.New.pf_type_of gl in
+    let reduce_to_atomic_ind = pf_apply Tacred.reduce_to_atomic_ind gl in
+    let type_of = pf_type_of gl in
     begin
       try
         Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
@@ -543,12 +543,12 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
 
 let invIn k names ids id =
   Proofview.Goal.enter begin fun gl ->
-    let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
+    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
     let nb_prod_init = nb_prod concl in
     let intros_replace_ids =
       Proofview.Goal.raw_enter begin fun gl ->
-        let concl = Tacmach.New.pf_nf_concl gl in
+        let concl = pf_nf_concl gl in
         let nb_of_new_hyp =
           nb_prod concl - (List.length hyps + nb_prod_init)
         in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3e35b0a4b..4e42bff7f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -380,6 +380,9 @@ module New = struct
   let tclFAIL lvl msg =
     tclZERO (Refiner.FailError (lvl,lazy msg))
 
+  let tclZEROMSG msg =
+    tclZERO (UserError ("", msg))
+
   let catch_failerror e =
     try
       Refiner.catch_failerror e;
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ceaa6f27c..0e4c1eb73 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -194,6 +194,10 @@ module New : sig
      (meaning that it will jump over [n] error catching tacticals FROM
      THIS MODULE. *)
   val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
+
+  val tclZEROMSG : Pp.std_ppcmds -> unit tactic
+  (** Fail with a [User_Error] containing the given message. *)
+
   val tclOR : unit tactic -> unit tactic -> unit tactic
   val tclONCE : unit tactic -> unit tactic
   val tclEXACTLY_ONCE : unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c61192031..1f88ed645 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -46,9 +46,6 @@ open Proofview.Notations
 
 exception Bound
 
-let tclZEROMSG msg =
-  Proofview.tclZERO (UserError ("", msg))
-
 let nb_prod x =
   let rec count n c =
     match kind_of_term c with
@@ -724,7 +721,7 @@ let cut c =
       let r = Goal.bind c Goal.refine in
       Proofview.tclSENSITIVE r
     else
-      tclZEROMSG (str "Not a proposition or a type.")
+      Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
   end
 
 let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
@@ -1188,7 +1185,7 @@ let assumption =
     if only_eq then
       let hyps = Proofview.Goal.hyps gl in
       arec gl false hyps
-    else tclZEROMSG (str "No such assumption.")
+    else Tacticals.New.tclZEROMSG (str "No such assumption.")
   | (id, c, t)::rest ->
     let concl = Proofview.Goal.concl gl in
     let is_same_type =
@@ -3927,6 +3924,4 @@ module New = struct
       )
     end
 
-  let tclZEROMSG = tclZEROMSG
-
 end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f3c5e7d26..9f4f0e9ce 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -417,5 +417,4 @@ module New : sig
 
   open Proofview
   val exact_proof : Constrexpr.constr_expr -> unit tactic
-  val tclZEROMSG : Pp.std_ppcmds -> unit tactic
 end