A stronger invariant on the syntax of TacAssert, what allows for a

simpler re-printing of assert.

Also fixing the precedence for printing "by" clause.

9 files changed, 21 insertions, 24 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index c15ef0dd44..c0677d5e2a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'tacexpr option *
+      bool * 'tacexpr option option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index a72fb0d061..dc21fa8856 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -495,7 +495,7 @@ let rec intern_atomic lf ist x =
       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 (b,otac,ipat,c) ->
-      TacAssert (b,Option.map (intern_pure_tactic ist) otac,
+      TacAssert (b,Option.map (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/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 3716de2518..789e8d64b4 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1735,10 +1735,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
         in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
-        let tac = Option.map (interp_tactic ist) t in
+        let tac = Option.map (Option.map (interp_tactic ist)) t in
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
-          (TacAssert(b,Option.map ignore t,ipat,c))
+          (TacAssert(b,Option.map (Option.map ignore) t,ipat,c))
           (Tactics.forward b tac ipat' c)) sigma
       end }
   | TacGeneralize cl ->
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 2c3c76ef74..3d8f10e008 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -148,7 +148,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
   | TacAssert (b,otac,na,c) ->
-      TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c)
+      TacAssert (b,Option.map (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)
   | TacLetTac (id,c,clp,b,eqpat) ->
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index c0cae84c02..756958c2f0 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -96,7 +96,7 @@ let intro = Tactics.intro
 let assert_ ?by c =
   let tac = match by with
   | None -> None
-  | Some tac -> Some (tclCOMPLETE tac)
+  | Some tac -> Some (Some tac)
   in
   Proofview.tclINDEPENDENT (Tactics.forward true tac None c)
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 36fffd74fa..f2e1f904b9 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -480,10 +480,6 @@ GEXTEND Gram
     [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
   ;
   by_tactic:
-    [ [ "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
-      | -> TacId [] ] ]
-  ;
-  opt_by_tactic:
     [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
     | -> None ] ]
   ;
@@ -606,9 +602,9 @@ GEXTEND Gram
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
       | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5356cdee8a..3779a94120 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -567,8 +567,9 @@ module Make
     | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-  let pr_by_tactic prt tac =
-    spc() ++ keyword "by" ++ spc () ++ prt tac
+  let pr_by_tactic prt = function
+    | Some tac -> keyword "by" ++ spc () ++ prt tac
+    | None -> mt()
 
   let pr_hyp_location pr_id = function
     | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
@@ -871,7 +872,7 @@ module Make
           hov 1 (
             primitive (if b then "assert" else "enough") ++
               pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
-              pr_by_tactic (pr.pr_tactic ltop) tac
+              pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
           )
         | TacAssert (_,None,ipat,c) ->
           hov 1 (
@@ -937,7 +938,7 @@ module Make
           )
 
         (* Equality and inversion *)
-        | TacRewrite (ev,l,cl,by) ->
+        | TacRewrite (ev,l,cl,tac) ->
           hov 1 (
             primitive (with_evars ev "rewrite") ++ spc ()
             ++ prlist_with_sep
@@ -947,11 +948,7 @@ module Make
                   pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
               l
             ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
-            ++ (
-              match by with
-                | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
-                | None -> mt()
-            )
+            ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
           )
         | TacInversion (DepInversion (k,c,ids),hyp) ->
           hov 1 (
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 991922d909..2f24e55a57 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2676,6 +2676,9 @@ let forward b usetac ipat c =
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
   | Some tac ->
+      let tac = match tac with
+        | None -> Tacticals.New.tclIDTAC
+        | Some tac -> Tacticals.New.tclCOMPLETE tac in
       if b then
         Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
       else
@@ -2683,8 +2686,8 @@ let forward b usetac ipat c =
           (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
 
 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
+let assert_by na t tac = forward true (Some (Some tac)) (ipat_of_name na) t
+let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 
 (***************************)
 (*  Generalization tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fa7b6791ea..142fdd3ebc 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -366,7 +366,7 @@ val pose_proof : Name.t -> constr ->
 
 (** Common entry point for user-level "assert", "enough" and "pose proof" *)
 
-val forward   : bool -> unit Proofview.tactic option ->
+val forward   : bool -> unit Proofview.tactic option option ->
   intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactic cut, actually a modus ponens rule *)