aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/tacexpr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3993f1b371..33a96150c1 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -146,7 +146,6 @@ type 'a gen_atomic_tactic_expr =
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
- | TacCofix of Id.t option
| TacMutualCofix of Id.t * (Id.t * 'trm) list
| TacAssert of
bool * 'tacexpr option *