diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-12 22:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | e2d4490b12514362af8e1f0b8b89cf0550f78130 (patch) | |
| tree | ddb275621606524ccd6af7b5a9b94b36988041c0 /ltac/tacinterp.ml | |
| parent | 613d99b98d3c78213a69acdbf23c660764487300 (diff) | |
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.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 3716de251..789e8d64b 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 -> |