diff options
| author | Hugo Herbelin | 2014-08-02 09:30:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:21 +0200 |
| commit | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (patch) | |
| tree | ba0f92d3bf019d5cbf4c72b2f2b667457052f179 /grammar | |
| parent | f9517286637fd0891a3ac1aac041b437e157f756 (diff) | |
Adding a syntax "enough" for the variant of "assert" with the order of
subgoals and the role of the "by tac" clause swapped.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index d1f4587915..2690cf8670 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -336,9 +336,10 @@ let rec mlexpr_of_atomic_tactic = function let l = mlexpr_of_list f l in <:expr< Tacexpr.TacMutualCofix $id$ $l$ >> - | Tacexpr.TacAssert (t,ipat,c) -> + | Tacexpr.TacAssert (b,t,ipat,c) -> let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in - <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ + <:expr< Tacexpr.TacAssert $mlexpr_of_bool b$ + $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> <:expr< Tacexpr.TacGeneralize |