From 455d5ee36dc36cbf094ddccf43059cddceedcd1f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 22 Dec 2013 02:32:49 +0100
Subject: Notations now accept the $(...)$ tactic-in-term syntax. They are
 resolved at internalization time.

---
 intf/notation_term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index ac5e0f5f9c..daf605ab28 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -24,7 +24,7 @@ type notation_constr =
   | NRef of global_reference
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
-  | NHole of Evar_kinds.t
+  | NHole of Evar_kinds.t * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
-- 
cgit v1.2.3