diff options
| author | Samuel Gruetter | 2021-03-19 16:31:35 -0400 |
|---|---|---|
| committer | Samuel Gruetter | 2021-03-19 16:31:35 -0400 |
| commit | 2420764db089d731635787bc11bd9ab312250fe7 (patch) | |
| tree | b61a068af969d23e31fff26b735dab63c37b6d04 /user-contrib/Ltac2/Init.v | |
| parent | fcfeb5bc45febe1a05f44a0a77b43be6b6905f35 (diff) | |
implement is_const, is_var, ... etc and has_evar for Ltac2
Fixes #13963
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. *) |