From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

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

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 5a563bf953..3a643b99b2 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
-- 
cgit v1.2.3


From 4d25b224b91959b85fcd68c825a307ec684f0bac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 28 Feb 2016 18:28:14 +0100
Subject: Printing notations: Cleaning in anticipation of fixing #4592.

- Making a clear distinction between expressions of the notation which
  are associated to binding variables only (as in `Notation "'lam' x ,
  P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
  (fun x:t => p) (fun x:t => q))') and those which are associated to
  at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
  "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
  as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
  and "Name id" as "GVar id".

There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
---
 intf/notation_term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 3a643b99b2..39a36310d1 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -61,7 +61,7 @@ type subscopes = tmp_scope_name option * scope_name list
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
 type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
 
 (** Type of variables when interpreting a constr_expr as an notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
-- 
cgit v1.2.3