From bde36d4b00185065628324d8ca71994f84eae244 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 12 Apr 2016 22:25:26 +0200
Subject: In the short term, stronger invariant on the syntax of TacAssert,
 what allows for a simpler re-printing of assert.

Also fixing the precedence for printing "by" clause.
---
 ltac/tacintern.ml | 2 +-
 ltac/tacinterp.ml | 4 ++--
 ltac/tacsubst.ml  | 3 ++-
 ltac/tauto.ml     | 2 +-
 4 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 15589d5c4..4917c3bb5 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -502,7 +502,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 9b41a276b..b875fb26f 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1765,10 +1765,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 438219f5a..22660aa83 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -151,7 +151,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 a86fdb98a..fa65a02b4 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -99,7 +99,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)
 
-- 
cgit v1.2.3