Removing useless tactic compatibility layer in Rewrite.

3 files changed, 54 insertions, 64 deletions

diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 7a20975158..82b79c883d 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -106,17 +106,11 @@ END
 let db_strat db = StratUnary (Topdown, StratHints (false, db))
 let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
 
-let cl_rewrite_clause_db = 
-  if Flags.profile then
-    let key = Profile.declare_profile "cl_rewrite_clause_db" in
-      Profile.profile3 key cl_rewrite_clause_db
-  else cl_rewrite_clause_db
-
 TACTIC EXTEND rewrite_strat
-| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s (Some id)) ]
-| [ "rewrite_strat" rewstrategy(s) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_strat s None) ]
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db (Some id)) ]
-| [ "rewrite_db" preident(db) ] -> [ Proofview.V82.tactic (cl_rewrite_clause_db db None) ]
+| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
+| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
+| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
 END
 
 let clsubstitute o c =
@@ -125,7 +119,7 @@ let clsubstitute o c =
       (fun cl ->
         match cl with
           | Some id when is_tac id -> tclIDTAC
-          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
 
 TACTIC EXTEND substitute
 | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
@@ -136,15 +130,15 @@ END
 
 TACTIC EXTEND setoid_rewrite
    [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-   -> [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences None) ]
+   -> [ cl_rewrite_clause c o AllOccurrences None ]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-      [ Proofview.V82.tactic (cl_rewrite_clause c o AllOccurrences (Some id))]
+      [ cl_rewrite_clause c o AllOccurrences (Some id) ]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-      [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) None)]
+      [ cl_rewrite_clause c o (occurrences_of occ) None ]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
-      [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
-      [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 8cc50684e2..cf59b6dc1f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -15,7 +15,7 @@ open Namegen
 open Term
 open Vars
 open Reduction
-open Tacticals
+open Tacticals.New
 open Tacmach
 open Tactics
 open Pretype_errors
@@ -625,7 +625,7 @@ let solve_remaining_by env sigma holes by =
     | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
       Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
     in
-    let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in
+    let solve_tac = tclCOMPLETE solve_tac in
     let solve sigma evk =
       let evi =
         try Some (Evd.find_undefined sigma evk)
@@ -1576,7 +1576,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Tacticals.New.tclTHENLIST [
+            let tac = tclTHENLIST [
               Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
               beta_hyp id;
               Proofview.Unsafe.tclNEWGOALS gls;
@@ -1632,23 +1632,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   end }
 
 let tactic_init_setoid () = 
-  try init_setoid (); tclIDTAC
-  with e when CErrors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
+  try init_setoid (); Proofview.tclUNIT ()
+  with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
 
 let cl_rewrite_clause_strat progress strat clause =
-  tclTHEN (tactic_init_setoid ())
-  ((if progress then tclWEAK_PROGRESS else fun x -> x)
-   (fun gl -> 
-    try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
-    with RewriteFailure e ->
-	 errorlabstrm "" (str"setoid rewrite failed: " ++ e)
+  tactic_init_setoid () <*>
+  (if progress then Proofview.tclPROGRESS else fun x -> x)
+   (Proofview.tclOR
+      (cl_rewrite_clause_newtac ~progress strat clause)
+      (fun (e, info) -> match e with
+       | RewriteFailure e ->
+	 tclZEROMSG (str"setoid rewrite failed: " ++ e)
        | Refiner.FailError (n, pp) -> 
-	  tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
+	  tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
+       | e -> Proofview.tclZERO ~info e))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
-let cl_rewrite_clause l left2right occs clause gl =
+let cl_rewrite_clause l left2right occs clause =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
-    cl_rewrite_clause_strat true strat clause gl
+    cl_rewrite_clause_strat true strat clause
 
 (** Setoid rewriting when called with "rewrite_strat" *)
 let cl_rewrite_clause_strat strat clause =
@@ -2028,12 +2030,12 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
   abs, sigma, res, Sorts.is_prop sort
 
 let get_hyp gl (c,l) clause l2r =
-  let evars = project gl in
-  let env = pf_env gl in
+  let evars = Tacmach.New.project gl in
+  let env = Tacmach.New.pf_env gl in
   let sigma, hi = decompose_applied_relation env evars (c,l) in
   let but = match clause with
-    | Some id -> pf_get_hyp_typ gl id 
-    | None -> Evarutil.nf_evar evars (pf_concl gl)
+    | Some id -> Tacmach.New.pf_get_hyp_typ id gl
+    | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl)
   in
   unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
 
@@ -2043,7 +2045,8 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 (* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
 
 (** Setoid rewriting when called with "rewrite" *)
-let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
+let general_s_rewrite cl l2r occs (c,l) ~new_goals =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
@@ -2054,31 +2057,25 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
     (), res
 	      }
   in
-  let origsigma = project gl in
-  init_setoid ();
-    try
-      tclWEAK_PROGRESS 
+  let origsigma = Tacmach.New.project gl in
+  tactic_init_setoid () <*>
+    Proofview.tclOR
+      (tclPROGRESS
 	(tclTHEN
-           (Refiner.tclEVARS evd)
-	   (Proofview.V82.of_tactic
-	    (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl
-    with RewriteFailure e ->
-      tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
-
-let general_s_rewrite_clause x =
-  match x with
-    | None -> general_s_rewrite None
-    | Some id -> general_s_rewrite (Some id)
-
-let general_s_rewrite_clause x y z w ~new_goals =
-  Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
+           (Proofview.Unsafe.tclEVARS evd)
+	    (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
+    (fun (e, info) -> match e with
+    | RewriteFailure e ->
+      tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+    | e -> Proofview.tclZERO ~info e)
+  end }
 
-let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
+let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let not_declared env ty rel =
-  Tacticals.New.tclFAIL 0
+  tclFAIL 0
     (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
@@ -2116,8 +2113,7 @@ let setoid_proof ty fn fallback =
   end }
 
 let tac_open ((evm,_), c) tac = 
-  Proofview.V82.tactic 
-    (tclTHEN (Refiner.tclEVARS evm) (tac c))
+    (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c))
 
 let poly_proof getp gett env evm car rel =
   if Sorts.is_prop (sort_of_rel env evm rel) then
@@ -2130,7 +2126,7 @@ let setoid_reflexivity =
      tac_open (poly_proof PropGlobal.get_reflexive_proof
 			  TypeGlobal.get_reflexive_proof
 			  env evm car rel)
-	      (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c))))
+	      (fun c -> tclCOMPLETE (apply c)))
     (reflexivity_red true)
 
 let setoid_symmetry =
@@ -2139,7 +2135,7 @@ let setoid_symmetry =
       tac_open
 	(poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
 	   env evm car rel)
-	(fun c -> Proofview.V82.of_tactic (apply c)))
+	(fun c -> apply c))
     (symmetry_red true)
     
 let setoid_transitivity c =
@@ -2148,8 +2144,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 -> Proofview.V82.of_tactic (eapply proof)
-	| Some c -> Proofview.V82.of_tactic (apply_with_bindings (proof,ImplicitBindings [ c ]))))
+	| None -> eapply proof
+	| Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])))
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
@@ -2167,9 +2163,9 @@ let setoid_symmetry_in id =
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
    Proofview.V82.of_tactic
-    (Tacticals.New.tclTHENLAST
+    (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
-      (Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
+      (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
       gl)
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index 01709f29fb..f448c85430 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -63,12 +63,12 @@ val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
 
 (** Entry point for user-level "rewrite_strat" *)
-val cl_rewrite_clause_strat : strategy -> Id.t option -> tactic
+val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
 
 (** Entry point for user-level "setoid_rewrite" *)
 val cl_rewrite_clause :
   interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
-  bool -> Locus.occurrences -> Id.t option -> tactic
+  bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
 
 val is_applied_rewrite_relation :
   env -> evar_map -> Context.Rel.t -> constr -> types option