From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 20:05:03 +0200
Subject: Allows recursive patterns for binders to be associative on the left.

This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.

Example of (artificial) notation that this commit supports:

  Notation "! x .. y # A #" :=
    (.. (A,(forall x, True)) ..,(forall y, True))
    (at level 200, x binder).
---
 interp/reserve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/reserve.ml')

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 22c5a2f5e5..04710282f5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -71,7 +71,7 @@ let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+  | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | _ -> Oth, None
 
-- 
cgit v1.2.3