diff options
| author | Pierre-Marie Pédrot | 2014-11-09 21:04:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-09 21:04:56 +0100 |
| commit | 2070c302639e841aae1558e8bc59cca6da099bdd (patch) | |
| tree | 991c54cf03e8e380714308a3ec154137b6cd7de4 /grammar | |
| parent | 90c398a7377ac4dbab5ed3add3cbbe9a1bea538a (diff) | |
Removing a unused boolean in the TacMove node of tacexpr 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 816502c1e5..02becc4967 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -387,8 +387,8 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacClearBody l -> let l = mlexpr_of_list (mlexpr_of_hyp) l in <:expr< Tacexpr.TacClearBody $l$ >> - | Tacexpr.TacMove (dep,id1,id2) -> - <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ + | Tacexpr.TacMove (id1,id2) -> + <:expr< Tacexpr.TacMove $mlexpr_of_hyp id1$ $mlexpr_of_move_location mlexpr_of_hyp id2$ >> |