diff options
| author | Michael Soegtrop | 2019-06-19 13:12:53 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2019-06-19 13:12:53 +0200 |
| commit | 8137e40af8f604fc4c82bbf85e32ba232491047d (patch) | |
| tree | 081da7eea209741db729022a3baa3c23206f5d02 /user-contrib/Ltac2/Init.v | |
| parent | 01d0b60694e3b4ee810bdde7115b40e49355ac24 (diff) | |
Removed backtracking and default variants of various functions and added option combinators
Diffstat (limited to 'user-contrib/Ltac2/Init.v')
| -rwxr-xr-x | 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 5c51c798c1..7c735f3b10 100755 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -63,6 +63,9 @@ Ltac2 Type exn ::= [ Not_focussed ]. Ltac2 Type exn ::= [ Not_found ]. (** Used when something is missing. *) +Ltac2 Type exn ::= [ No_value ]. +(** Used for empty lists, None options and the like. *) + Ltac2 Type exn ::= [ Match_failure ]. (** Used to signal a pattern didn't match a term. *) |