aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-09 21:04:56 +0100
committerPierre-Marie Pédrot2014-11-09 21:04:56 +0100
commit2070c302639e841aae1558e8bc59cca6da099bdd (patch)
tree991c54cf03e8e380714308a3ec154137b6cd7de4 /intf
parent90c398a7377ac4dbab5ed3add3cbbe9a1bea538a (diff)
Removing a unused boolean in the TacMove node of tacexpr AST.
Diffstat (limited to 'intf')
-rw-r--r--intf/tacexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7844f74e2b..efe62f569c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
(* Context management *)
| TacClear of bool * 'nam list
| TacClearBody of 'nam list
- | TacMove of bool * 'nam * 'nam move_location
+ | TacMove of 'nam * 'nam move_location
| TacRename of ('nam *'nam) list
(* Trmuctors *)