Writing [cut] tactic using the new monad.

5 files changed, 21 insertions, 23 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a34cbf70f..b086190f4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -477,11 +477,9 @@ let f_equal =
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         let ty = Termops.refresh_universes (type_of c1) in
-        Proofview.V82.tactic begin
-          tclTHENTRY
-            (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
-            (simple_reflexivity ())
-        end
+        Tacticals.New.tclTRY (Tacticals.New.tclTHEN
+          (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
+          (Tacticals.New.tclTRY (Proofview.V82.tactic (simple_reflexivity ()))))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e856326c8..fe22708a0 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -141,7 +141,7 @@ let left_instance_tac (inst,id) continue seq=
 	if lookup (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (cut dom)
+	  tclTHENS (Proofview.V82.of_tactic (cut dom))
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
 		(fun gls->generalize
@@ -175,7 +175,7 @@ let left_instance_tac (inst,id) continue seq=
 let right_instance_tac inst continue seq=
   match inst with
       Phantom dom ->
-	tclTHENS (cut dom)
+	tclTHENS (Proofview.V82.of_tactic (cut dom))
 	[tclTHENLIST
 	   [Proofview.V82.of_tactic introf;
 	    (fun gls->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 99e03cdbe..6d9af2bbf 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -144,12 +144,12 @@ let ll_arrow_tac a b c backtrack id continue seq=
 		  mkApp ((constr_of_global id),
 			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (cut c)
+      (tclTHENS (Proofview.V82.of_tactic (cut c))
 	 [tclTHENLIST
 	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (cut cc)
+	  tclTHENS (Proofview.V82.of_tactic (cut cc))
             [exact_no_check (constr_of_global id);
 	     tclTHENLIST
 	       [generalize [d];
@@ -184,7 +184,7 @@ let left_exists_tac ind backtrack id continue seq gls=
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
-    (tclTHENS (cut prod)
+    (tclTHENS (Proofview.V82.of_tactic (cut prod))
        [tclTHENLIST
 	  [Proofview.V82.of_tactic intro;
 	   (fun gls->
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index d49f225e6..2a5e81ec0 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -616,7 +616,7 @@ let rec fourier gl=
 					 )
 				]));
                        !tac1]);
-	   tac:=(tclTHENS (cut (get coq_False))
+	   tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False)))
 				  [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None));
 				   !tac])
       |_-> assert false) |_-> assert false
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 98baf7b2a..e4e3650c7 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1077,7 +1077,7 @@ let replay_history tactic_normalisation =
 	  let state_eg = mk_eq eq1 rhs in
 	  let tac = scalar_norm_add [P_APP 3] e2.body in
 	  Tacticals.New.tclTHENS
-	    (Proofview.V82.tactic (cut state_eg))
+	    (cut state_eg)
 	    [ Tacticals.New.tclTHENS
 	        (Tacticals.New.tclTHENLIST [
 		  (intros_using [aux]);
@@ -1086,9 +1086,9 @@ let replay_history tactic_normalisation =
 		      [| eq1; rhs; mkVar aux; mkVar id |])]);
 		  Proofview.V82.tactic (clear [aux;id]);
 		  (intros_using [id]);
-		  Proofview.V82.tactic (cut (mk_gt kk dd)) ])
+		  (cut (mk_gt kk dd)) ])
 	        [ Tacticals.New.tclTHENS
-		    (Proofview.V82.tactic (cut (mk_gt kk izero)))
+		    (cut (mk_gt kk izero))
 		    [ Tacticals.New.tclTHENLIST [
 		        (intros_using [aux1; aux2]);
 		        (Proofview.V82.tactic (generalize_tac
@@ -1115,8 +1115,8 @@ let replay_history tactic_normalisation =
 	  and dd = mk_integer d in
 	  let tac = scalar_norm_add [P_APP 2] e2.body in
 	  Tacticals.New.tclTHENS
-	    (Proofview.V82.tactic (cut (mk_gt dd izero)))
-	    [ Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk dd)))
+	    (cut (mk_gt dd izero))
+	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
 		[Tacticals.New.tclTHENLIST [
 		  (intros_using [aux2;aux1]);
 		  Proofview.V82.tactic (generalize_tac
@@ -1146,7 +1146,7 @@ let replay_history tactic_normalisation =
 	  if e1.kind == DISE then
             let tac = scalar_norm [P_APP 3] e2.body in
             Tacticals.New.tclTHENS
-	      (Proofview.V82.tactic (cut state_eq))
+	      (cut state_eq)
 	      [Tacticals.New.tclTHENLIST [
 		(intros_using [aux1]);
 		Proofview.V82.tactic (generalize_tac
@@ -1158,10 +1158,10 @@ let replay_history tactic_normalisation =
 	       Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
 	  else
             let tac = scalar_norm [P_APP 3] e2.body in
-            Tacticals.New.tclTHENS (Proofview.V82.tactic (cut state_eq))
+            Tacticals.New.tclTHENS (cut state_eq)
 	      [
 		Tacticals.New.tclTHENS
-		 (Proofview.V82.tactic (cut (mk_gt kk izero)))
+		 (cut (mk_gt kk izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   Proofview.V82.tactic (generalize_tac
@@ -1188,7 +1188,7 @@ let replay_history tactic_normalisation =
             scalar_norm [P_APP 3] e1.body
 	  in
 	  Tacticals.New.tclTHENS
-	    (Proofview.V82.tactic (cut (mk_eq eq1 (mk_inv eq2))))
+	    (cut (mk_eq eq1 (mk_inv eq2)))
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
 	      Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
@@ -1221,7 +1221,7 @@ let replay_history tactic_normalisation =
             shuffle_mult_right p_initial
               orig.body m ({c= negone;v= v}::def.body) in
 	  Tacticals.New.tclTHENS
-	    (Proofview.V82.tactic (cut theorem))
+	    (cut theorem)
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
 	      (elim_id aux);
@@ -1277,9 +1277,9 @@ let replay_history tactic_normalisation =
 	    and kk2 = mk_integer k2 in
 	    let p_initial = [P_APP 2;P_TYPE] in
 	    let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
-            Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk1 izero)))
+            Tacticals.New.tclTHENS (cut (mk_gt kk1 izero))
 	      [Tacticals.New.tclTHENS
-		 (Proofview.V82.tactic (cut (mk_gt kk2 izero)))
+		 (cut (mk_gt kk2 izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   Proofview.V82.tactic (generalize_tac