From 6d8b31504efce96ec6d3011763ced0c631cf576a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 20:35:19 +0200
Subject: Don't reuse Coq AST for binding quotations.

This allows antiquotations in binding lists.
---
 src/tac2qexpr.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 794281cc75..b68efe73ac 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -9,6 +9,7 @@
 open Util
 open Loc
 open Names
+open Tac2expr
 
 (** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
     sometimes allow anti-quotations. Used for notation scopes. *)
@@ -17,6 +18,11 @@ type 'a or_anti =
 | QExpr of 'a
 | QAnti of Id.t located
 
+type bindings =
+| QImplicitBindings of raw_tacexpr list
+| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * raw_tacexpr) Loc.located list
+| QNoBindings
+
 type intro_pattern =
 | QIntroForthcoming of bool
 | QIntroNaming of intro_pattern_naming
-- 
cgit v1.2.3