diff options
| author | Pierre-Marie Pédrot | 2017-07-26 21:27:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-27 01:39:24 +0200 |
| commit | f204058d329fa78b506f4c3b3c4f97ecce504d4b (patch) | |
| tree | 97ab8dee9941ddfaced5059456b6864d3beb3cac /theories/Init.v | |
| parent | c9e7d7f1ceb22667e77a4ee49a4afc2cce6f9a2c (diff) | |
Adding necessary primitives to do pattern-matching over constr.
Diffstat (limited to 'theories/Init.v')
| -rw-r--r-- | theories/Init.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Init.v b/theories/Init.v index c0a73576d3..803e48e352 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -27,6 +27,7 @@ Ltac2 Type constant. Ltac2 Type inductive. Ltac2 Type constructor. Ltac2 Type projection. +Ltac2 Type pattern. Ltac2 Type constr. Ltac2 Type message. @@ -56,3 +57,6 @@ Ltac2 Type exn ::= [ Not_focussed ]. Ltac2 Type exn ::= [ Not_found ]. (** Used when something is missing. *) + +Ltac2 Type exn ::= [ Match_failure ]. +(** Used to signal a pattern didn't match a term. *) |