diff options
| author | Pierre-Marie Pédrot | 2014-06-06 15:21:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-06 15:32:36 +0200 |
| commit | 3b83b311798f0d06444e1994602e0b531e207ef5 (patch) | |
| tree | 8d41bca774ee92bfa2c9866cc54ef4d7acd5a20c /grammar | |
| parent | ce85edee592fef31575e138af2945ce8be74cd07 (diff) | |
Moving the [split] tactic out of the AST.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index cada607f67..528678d1d3 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -385,9 +385,9 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_move_location mlexpr_of_hyp id2$ >> (* Constructors *) - | Tacexpr.TacSplit (ev,b,l) -> + | Tacexpr.TacSplit (ev,l) -> <:expr< Tacexpr.TacSplit - ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>> + ($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>> | Tacexpr.TacAnyConstructor (ev,t) -> <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>> | Tacexpr.TacConstructor (ev,n,l) -> |