Adding a syntax "enough" for the variant of "assert" with the order of

subgoals and the role of the "by tac" clause swapped.

5 files changed, 21 insertions, 11 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c2f85d534..e2f87062e 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -473,8 +473,8 @@ let rec intern_atomic lf ist x =
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacAssert (otac,ipat,c) ->
-      TacAssert (Option.map (intern_pure_tactic ist) otac,
+  | TacAssert (b,otac,ipat,c) ->
+      TacAssert (b,Option.map (intern_pure_tactic ist) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen false (not (Option.is_empty otac)) ist c)
   | TacGeneralize cl ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e0d24e9e1..b52a3e7e9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1610,7 +1610,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	  (Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
           gl
       end
-  | TacAssert (t,ipat,c) ->
+  | TacAssert (b,t,ipat,c) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1620,7 +1620,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let patt = interp_intro_pattern ist env in
         Tacticals.New.tclTHEN
           (Proofview.V82.tclEVARS sigma)
-          (Tactics.forward (Option.map (interp_tactic ist) t)
+          (Tactics.forward b (Option.map (interp_tactic ist) t)
               (Option.map patt ipat) c)
       end
   | TacGeneralize cl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 30fffed91..428061463 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacCofix idopt as x -> x
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacAssert (b,na,c) ->
-      TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
+  | TacAssert (b,otac,na,c) ->
+      TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 442f0a3cb..cb6894fef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+let a = 1
+
 open Pp
 open Errors
 open Util
@@ -1738,6 +1740,7 @@ let assert_as first ipat c =
   end
 
 let assert_tac na = assert_as true (ipat_of_name na)
+let enough_tac na = assert_as false (ipat_of_name na)
 
 (* apply in as *)
 
@@ -1856,7 +1859,7 @@ let letin_pat_tac with_eq name c occs =
   letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
-let forward usetac ipat c =
+let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.raw_enter begin fun gl ->
@@ -1864,10 +1867,15 @@ let forward usetac ipat c =
       Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
-      Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
+      if b then
+        Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+      else
+        Tacticals.New.tclTHENS3PARTS
+          (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
-let pose_proof na c = forward None (ipat_of_name na) c
-let assert_by na t tac = forward (Some tac) (ipat_of_name na) t
+let pose_proof na c = forward true None (ipat_of_name na) c
+let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
+let enough_by na t tac = forward false (Some tac) (ipat_of_name na) t
 
 (***************************)
 (*  Generalization tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 20b974a82..c2403d97a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -334,13 +334,15 @@ val assert_replacing            : Id.t -> types -> tactic -> tactic
 val cut_replacing               : Id.t -> types -> tactic -> 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
+val forward   : bool -> unit Proofview.tactic option -> intro_pattern_expr located option -> constr -> unit Proofview.tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> Name.t ->
   constr -> types option -> clause -> unit Proofview.tactic
 val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t ->
   evar_map * constr -> clause -> unit Proofview.tactic
 val assert_tac : Name.t -> types -> unit Proofview.tactic
+val enough_tac : Name.t -> types -> unit Proofview.tactic
 val assert_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
+val enough_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
 val pose_proof : Name.t -> constr -> unit Proofview.tactic
 
 val generalize      : constr list -> tactic