Writing [cut] tactic using the new monad.

13 files changed, 81 insertions, 68 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a34cbf70fd..b086190f4e 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 e856326c84..fe22708a06 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 99e03cdbea..6d9af2bbfb 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 d49f225e67..2a5e81ec0d 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 98baf7b2a5..e4e3650c73 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
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0198fc3fdf..c6fb0d12aa 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -25,9 +25,9 @@ let absurd c gls =
   let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
   let c = j.Environ.utj_val in
   (tclTHENS
-     (tclTHEN (elim_type (build_coq_False ())) (cut c))
+     (tclTHEN (elim_type (build_coq_False ())) (Proofview.V82.of_tactic (cut c)))
      ([(tclTHENS
-          (cut (mkApp(build_coq_not (),[|c|])))
+          (Proofview.V82.of_tactic (cut (mkApp(build_coq_not (),[|c|]))))
 	  ([(tclTHEN (Proofview.V82.of_tactic intros)
 	       ((fun gl ->
 		   let ida = pf_nth_hyp_id gl 1
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9c1107bebc..f5f09f27ec 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -90,7 +90,7 @@ let general_decompose recognizer c =
   let type_of = Tacmach.New.pf_type_of gl in
   try (* type_of can raise exceptions *)
   let typc = type_of c in
-  Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
+  Tacticals.New.tclTHENS (cut typc)
     [ Tacticals.New.tclTHEN (intro_using tmphyp_name)
          (Tacticals.New.onLastHypId
 	    (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer)
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index cb518a03a3..a98cb2a6f1 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -190,7 +190,7 @@ let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality
 let decideEquality rectype =
   Proofview.Goal.enter begin fun gl ->
   let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in
-  (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide)) [default_auto;decideEqualityGoal])
+  (Tacticals.New.tclTHENS (cut decide) [default_auto;decideEqualityGoal])
   end
 
 
@@ -200,7 +200,7 @@ let compare c1 c2 =
   Proofview.Goal.enter begin fun gl ->
   let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in
   let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in
-  (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide))
+  (Tacticals.New.tclTHENS (cut decide)
             [(Tacticals.New.tclTHEN  intro
              (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case)
                        (Proofview.V82.tactic clear_last)));
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c72d8ad50..098e45a4aa 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1195,11 +1195,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   if List.is_empty injectors then
     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
   else
-    Tacticals.New.tclTHEN
-      (Proofview.V82.tactic (tclMAP
-         (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
-         (if l2r then List.rev injectors else injectors)))
-      (tac (List.length injectors))
+    Proofview.tclBIND
+      (Proofview.list_map
+         (fun (pf,ty) -> Tacticals.New.tclTHENS (cut ty) [Proofview.tclUNIT (); Proofview.V82.tactic (refine pf)])
+         (if l2r then List.rev injectors else injectors))
+      (fun _ -> tac (List.length injectors))
 
 exception Not_dep_pair
 
@@ -1230,7 +1230,7 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
       (* cut with the good equality and prove the requested goal *)
-    tclTHENS (cut (mkApp (ceq,new_eq_args)))
+    tclTHENS (Proofview.V82.of_tactic (cut (mkApp (ceq,new_eq_args))))
       [tclIDTAC; tclTHEN (apply (
         mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
        )) (Proofview.V82.of_tactic (Auto.trivial [] []))
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2e3b6e1af7..9934e3a00a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1833,7 +1833,7 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-    Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp))
+    Tacticals.New.tclTHENS (Tactics.cut new_hyp)
       [ Proofview.V82.tactic (intro_replacing id);
 	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ]
   end
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e5f69378f4..63e1e79db0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1577,12 +1577,13 @@ and interp_atomic ist tac =
           gl
       end
   | TacCut c ->
-      Proofview.V82.tactic begin fun gl -> 
-        let (sigma,c_interp) = pf_interp_type ist gl c in
-        tclTHEN
-	  (tclEVARS sigma)
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
+        let (sigma, c_interp) = interp_type ist env sigma c in
+        Tacticals.New.tclTHEN
+	  (Proofview.V82.tclEVARS sigma)
 	  (Tactics.cut c_interp)
-          gl
       end
   | TacAssert (t,ipat,c) ->
       Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 969f9ef553..11ad1aad14 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -48,6 +48,9 @@ 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
@@ -695,18 +698,40 @@ let resolve_classes gl =
 (*     Cut tactics        *)
 (**************************)
 
-let cut c gl =
-  match kind_of_term (pf_hnf_type_of gl c) with
-    | Sort _ ->
-        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-        let t = mkProd (Anonymous, c, pf_concl gl) in
-          tclTHENFIRST
-            (internal_cut_rev id c)
-            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
-            gl
-    | _  -> error "Not a proposition or a type."
+let cut c =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let concl = Proofview.Goal.concl gl in
+    let is_sort =
+      try
+        (** Backward compat: ensure that [c] is well-typed. *)
+        let typ = Typing.type_of env sigma c in
+        let typ = whd_betadeltaiota env sigma typ in
+        match kind_of_term typ with
+        | Sort _ -> true
+        | _ -> false
+      with e when Pretype_errors.precatchable_exception e -> false
+    in
+    if is_sort then
+      let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
+      (** Backward compat: normalize [c]. *)
+      let c = local_strong whd_betaiota sigma c in
+      let c = Goal.Refinable.make begin fun h ->
+        let f = Goal.Refinable.mkEvar h env (mkArrow c (Vars.lift 1 concl)) in
+        let x = Goal.Refinable.mkEvar h env c in
+        Goal.bind f (fun f -> Goal.bind x (fun x ->
+          let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
+          Goal.return (mkApp (f, [|x|]))
+        ))
+      end in
+      let r = Goal.bind c Goal.refine in
+      Proofview.tclSENSITIVE r
+    else
+      tclZEROMSG (str "Not a proposition or a type.")
+  end
 
-let cut_intro t = Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut t)) intro
+let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro
 
 (* [assert_replacing id T tac] adds the subgoals of the proof of [T]
    before the current goal
@@ -734,13 +759,6 @@ let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac
 
 let cut_replacing id t tac = tclTHENLAST (internal_cut_rev_replace id t) tac
 
-let cut_in_parallel l =
-  let rec prec = function
-    | [] -> tclIDTAC
-    | h::t -> tclTHENFIRST (cut h) (prec t)
-  in
-    prec (List.rev l)
-
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
@@ -1166,9 +1184,6 @@ let exact_proof c gl =
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
   in refine_no_check c gl
 
-let tclZEROMSG msg =
-  Proofview.tclZERO (UserError ("", msg))
-
 let assumption =
   let rec arec gl only_eq = function
   | [] ->
@@ -1268,7 +1283,7 @@ let specialize mopt (c,lbind) g =
 	       (exact_no_check term)) g
        | _ -> tclTHEN tac
 	   (tclTHENLAST
-              (fun g -> cut (pf_type_of g term) g)
+              (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g)
               (exact_no_check term)) g
 
 (* Keeping only a few hypotheses *)
@@ -3641,7 +3656,7 @@ let prove_symmetry hdcncl eq_kind =
     | MonomorphicLeibnizEq (c1,c2) -> mkApp(hdcncl,[|c2;c1|])
     | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp(hdcncl,[|typ;c2;c1|])
     | HeterogenousEq (t1,c1,t2,c2) -> mkApp(hdcncl,[|t2;c2;t1;c1|]) in
-  Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut symc))
+  Tacticals.New.tclTHENFIRST (cut symc)
     (Tacticals.New.tclTHENLIST
       [ intro;
         Tacticals.New.onLastHyp simplest_case;
@@ -3703,7 +3718,7 @@ let symmetry_in id =
           | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
           | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
           | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
-        Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (it_mkProd_or_LetIn symccl sign)))
+        Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
           [ Proofview.V82.tactic (intro_replacing id);
             Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ]
     end
@@ -3751,8 +3766,8 @@ let prove_transitivity hdcncl eq_kind t =
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
   in
-  Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq2))
-    (Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq1))
+  Tacticals.New.tclTHENFIRST (cut eq2)
+    (Tacticals.New.tclTHENFIRST (cut eq1)
        (Tacticals.New.tclTHENLIST
 	  [ Tacticals.New.tclDO 2 intro;
 	    Tacticals.New.onLastHyp simplest_case;
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 21948f9ae7..b181dc5348 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -362,11 +362,10 @@ val transitivity                : constr -> unit Proofview.tactic
 val etransitivity               : unit Proofview.tactic
 val intros_transitivity         : constr option -> unit Proofview.tactic
 
-val cut                         : constr -> tactic
+val cut                         : constr -> unit Proofview.tactic
 val cut_intro                   : constr -> unit Proofview.tactic
 val assert_replacing            : Id.t -> types -> tactic -> tactic
 val cut_replacing               : Id.t -> types -> tactic -> tactic
-val cut_in_parallel             : constr list -> tactic
 
 val assert_as : bool -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
 val forward   : unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic