Put the "generalize" tactic in the monad.

1 files changed, 29 insertions, 29 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fc5054080..ab33a5d2c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1067,12 +1067,12 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 1;P_TYPE] in
 	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac
+	    generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
-		mkVar id1; mkVar id2 |])]);
+		mkVar id1; mkVar id2 |])];
 	    Proofview.V82.tactic (mk_then tac);
 	    (intros_using [aux]);
 	    Proofview.V82.tactic (resolve_id aux);
@@ -1104,7 +1104,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le)
+	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  let id = hyp_of_tag e1.id in
 	  let eq1 = val_of(decompile e1)
@@ -1119,7 +1119,7 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS
 	        (Tacticals.New.tclTHENLIST [
 		  (intros_using [aux]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
 		      [| eq1; rhs; mkVar aux; mkVar id |])]);
 		  (clear [aux;id]);
@@ -1129,9 +1129,9 @@ let replay_history tactic_normalisation =
 		    (cut (mk_gt kk izero))
 		    [ Tacticals.New.tclTHENLIST [
 		        (intros_using [aux1; aux2]);
-		        (Proofview.V82.tactic (generalize_tac
+		        (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
-			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
 		        (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
@@ -1157,7 +1157,7 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
 		[Tacticals.New.tclTHENLIST [
 		  (intros_using [aux2;aux1]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
                       [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
 		  (clear [aux1;aux2]);
@@ -1187,7 +1187,7 @@ let replay_history tactic_normalisation =
 	      (cut state_eq)
 	      [Tacticals.New.tclTHENLIST [
 		(intros_using [aux1]);
-		Proofview.V82.tactic (generalize_tac
+		(generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
                     [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
 		(clear [aux1;id]);
@@ -1202,7 +1202,7 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
 		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
 		   (clear [aux1;aux2;id]);
@@ -1229,7 +1229,7 @@ let replay_history tactic_normalisation =
 	    (cut (mk_eq eq1 (mk_inv eq2)))
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
-	      Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
 	      (clear [id1;id2;aux]);
 	      (intros_using [id]);
@@ -1265,7 +1265,7 @@ let replay_history tactic_normalisation =
 	      (elim_id aux);
 	      (clear [aux]);
 	      (intros_using [vid; aux]);
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
 	      Proofview.V82.tactic (mk_then tac);
@@ -1304,7 +1304,7 @@ let replay_history tactic_normalisation =
               if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
             let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
             Tacticals.New.tclTHENLIST [
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
 	      Proofview.V82.tactic (mk_then tac);
 	      (intros_using [id]);
@@ -1320,7 +1320,7 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk2 izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
 		       eq1;eq2;kk1;kk2;
 		       mkVar aux1;mkVar aux2;
@@ -1338,12 +1338,12 @@ let replay_history tactic_normalisation =
                 simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+	  Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
 	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
+	    (generalize_tac [mkVar (hyp_of_tag e)]);
             unfold sp_Zle;
 	    simpl_in_concl;
 	    unfold sp_not;
@@ -1366,7 +1366,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize p_initial t in
   let shift_left =
     tclTHEN
-      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
       (tclTRY (Proofview.V82.of_tactic (clear [id])))
   in
   if not (List.is_empty tac) then
@@ -1546,7 +1546,7 @@ let nat_inject =
 	  begin try match destructurate_prop t with
               Kapp(Le,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1555,7 +1555,7 @@ let nat_inject =
                 ]
             | Kapp(Lt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1564,7 +1564,7 @@ let nat_inject =
                 ]
             | Kapp(Ge,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1573,7 +1573,7 @@ let nat_inject =
                 ]
             | Kapp(Gt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1582,7 +1582,7 @@ let nat_inject =
                 ]
             | Kapp(Neq,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1592,7 +1592,7 @@ let nat_inject =
             | Kapp(Eq,[typ;t1;t2]) ->
 		if is_conv typ (Lazy.force coq_nat) then
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
 		    (explore [P_APP 3; P_TYPE] t2);
@@ -1723,7 +1723,7 @@ let destructure_hyps =
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit))))
@@ -1734,7 +1734,7 @@ let destructure_hyps =
               begin match destructurate_prop t with
 		Kapp(Or,[t1;t2]) ->
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
                       (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit))))
@@ -1742,7 +1742,7 @@ let destructure_hyps =
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1752,7 +1752,7 @@ let destructure_hyps =
 		  let d1 = decidability t1 in
 		  let d2 = decidability t2 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1764,7 +1764,7 @@ let destructure_hyps =
 		       For t1, being decidable implies being Prop. *)
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1773,7 +1773,7 @@ let destructure_hyps =
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
                   ]
@@ -1781,7 +1781,7 @@ let destructure_hyps =
 		  (try
 		     let thm = not_binop op in
                      Tacticals.New.tclTHENLIST [
-		       Proofview.V82.tactic (generalize_tac
+		       (generalize_tac
 			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 		       (onClearedName i (fun _ -> loop lit))
                      ]