From ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 28 Jul 2020 23:47:11 +0200
Subject: In recursive notations, accept partial application over the recursive
 pattern.

This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
---
 interp/notation.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 948ebe9640..1a361dc1a6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -391,6 +391,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+  | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+      RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
+  | NApp (NList (_,_,NApp (_,args),_,_), args') ->
+      Oth, AppBoundedNotation (List.length args + List.length args')
   | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
   | _ -> Oth, NotAppNotation
-- 
cgit v1.2.3