From c3be78f96b91a042944f9bee66bf0ea8d929a37d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 16:56:27 +0200
Subject: Introducing the all-mighty intro-patterns.

---
 src/tac2qexpr.mli | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 src/tac2qexpr.mli

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
new file mode 100644
index 0000000000..794281cc75
--- /dev/null
+++ b/src/tac2qexpr.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Loc
+open Names
+
+(** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
+    sometimes allow anti-quotations. Used for notation scopes. *)
+
+type 'a or_anti =
+| QExpr of 'a
+| QAnti of Id.t located
+
+type intro_pattern =
+| QIntroForthcoming of bool
+| QIntroNaming of intro_pattern_naming
+| QIntroAction of intro_pattern_action
+and intro_pattern_naming =
+| QIntroIdentifier of Id.t or_anti
+| QIntroFresh of Id.t or_anti
+| QIntroAnonymous
+and intro_pattern_action =
+| QIntroWildcard
+| QIntroOrAndPattern of or_and_intro_pattern
+| QIntroInjection of intro_pattern list
+(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
+| QIntroRewrite of bool
+and or_and_intro_pattern =
+| QIntroOrPattern of intro_pattern list list
+| QIntroAndPattern of intro_pattern list
-- 
cgit v1.2.3