diff options
| author | Jasper Hugunin | 2020-11-02 17:08:25 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2021-01-04 09:44:46 -0800 |
| commit | 70d557994583bd081787e28f68d627a0833eb9c0 (patch) | |
| tree | f363a0782c7395de8a0a2cf1755bd69c63faa614 /interp/notation.ml | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Remember universe instances of constants in notations
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 14 |
1 files changed, 7 insertions, 7 deletions
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 |