diff options
Diffstat (limited to 'user-contrib/Ltac2/Init.v')
| -rw-r--r-- | user-contrib/Ltac2/Init.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 097a0ca25f..19c89d7266 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -80,3 +80,6 @@ Ltac2 Type exn ::= [ Invalid_argument (message option) ]. Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) + +Ltac2 Type exn ::= [ Assertion_failure ]. +(** Used to indicate that an Ltac2 function ran into a situation that should never occcur. *) |