diff options
| author | Jason Gross | 2019-05-22 17:13:24 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-05-22 21:15:02 -0400 |
| commit | cd6db46a88eb192b7370308489cd4e2b719df342 (patch) | |
| tree | e2cee90d62edb0f65569a90b11a938fa27f5bf52 /user-contrib/Ltac2/Init.v | |
| parent | 5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff) | |
[Ltac2] Add util files for Bool, List, Option
Most functions are taken either from the Coq standard library or the
OCaml standard library. One (`enumerate`) is taken from Python. Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception). Since `exists` is a keyword, we use the
Coq name `existsb` instead. We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.
Note that `seq` matches neither Coq nor OCaml; it takes a `step`
argument for how much to increment by on each step.
Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?
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 dc1690bdfb..c47aa82b05 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -66,5 +66,8 @@ Ltac2 Type exn ::= [ Not_found ]. Ltac2 Type exn ::= [ Match_failure ]. (** Used to signal a pattern didn't match a term. *) +Ltac2 Type exn ::= [ Invalid_argument (message option) ]. +(** Used to signal that an invalid argument was passed to a tactic. *) + Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) |