aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 31e242c1f..a94da4331 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -207,7 +207,8 @@ let cases_pattern_key = function
let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
- | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args)
+ | AList (_,_,AApp (ARef ref,args),_,_)
+ | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args)
| ARef ref -> RefKey(make_gr ref), None
| _ -> Oth, None