From f204058d329fa78b506f4c3b3c4f97ecce504d4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 21:27:36 +0200
Subject: Adding necessary primitives to do pattern-matching over constr.

---
 theories/Init.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'theories/Init.v')

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. *)
-- 
cgit v1.2.3