diff options
author | 2016-04-27 22:13:04 +0200 | |
---|---|---|
committer | 2016-04-27 22:13:04 +0200 | |
commit | 32716cc80cbda47e59e26c920ffb0ab738b0e9c0 (patch) | |
tree | aa30dbcd367b5079f6308f9d9fad0c62b70bc964 /ltac | |
parent | cc3f28467f826506b8eb6e07c3b2db9ffd2ed3ba (diff) |
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
Diffstat (limited to 'ltac')
-rw-r--r-- | ltac/tacintern.ml | 2 | ||||
-rw-r--r-- | ltac/tacinterp.ml | 4 | ||||
-rw-r--r-- | ltac/tacsubst.ml | 3 | ||||
-rw-r--r-- | ltac/tauto.ml | 2 |
4 files changed, 5 insertions, 6 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 4917c3bb5..15589d5c4 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 (Option.map (intern_pure_tactic ist)) otac, + 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/ltac/tacinterp.ml b/ltac/tacinterp.ml index b875fb26f..9b41a276b 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 (Option.map (interp_tactic ist)) t in + let tac = Option.map (interp_tactic ist) t in Tacticals.New.tclWITHHOLES false (name_atomic ~env - (TacAssert(b,Option.map (Option.map ignore) t,ipat,c)) + (TacAssert(b,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 22660aa83..438219f5a 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -151,8 +151,7 @@ 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 (Option.map (subst_tactic subst)) otac,na, - subst_glob_constr subst 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) | TacLetTac (id,c,clp,b,eqpat) -> diff --git a/ltac/tauto.ml b/ltac/tauto.ml index fa65a02b4..a86fdb98a 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 (Some tac) + | Some tac -> Some (tclCOMPLETE tac) in Proofview.tclINDEPENDENT (Tactics.forward true tac None c) |