From 70d557994583bd081787e28f68d627a0833eb9c0 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 2 Nov 2020 17:08:25 -0800
Subject: Remember universe instances of constants in notations

---
 interp/notation.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index f2d113954b..33d96f0439 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -400,12 +400,12 @@ let cases_pattern_key c = match DAst.get c with
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
-  | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
+  | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
+  | NList (_,_,NApp (NRef (ref,_),args),_,_)
+  | 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') ->
+  | 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')
@@ -2353,8 +2353,8 @@ let browse_notation strict ntn map =
 
 let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
   match c with
-  | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
-  | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
+  | NRef (ref,_) when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
+  | NApp (NRef (ref,_), l) when head || List.for_all isNVar_or_NHole l && test ref ->
       Some (on_parsing,on_printing,ntn,sc,ref)
   | _ -> None
 
-- 
cgit v1.2.3