diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2expr.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2expr.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index 2e7dfc42db..af7bc32785 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -168,8 +168,6 @@ type strexpr = (** Syntactic extensions *) | StrMut of qualid * raw_tacexpr (** Redefinition of mutable globals *) -| StrRun of raw_tacexpr - (** Toplevel evaluation of an expression *) (** {5 Dynamic semantics} *) |