diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index f74413704b..5ddebf3c99 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -175,6 +175,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacClearBody of 'id list | TacMove of bool * 'id * 'id | TacRename of ('id *'id) list + | TacRevert of 'id list (* Constructors *) | TacLeft of 'constr bindings |