diff options
| author | coqbot-app[bot] | 2021-01-09 12:34:12 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-09 12:34:12 +0000 |
| commit | 723440611965ccdecfd56e61c8f1f8618a08841d (patch) | |
| tree | 9d3582f11361a788c7f60568fb95d112839eec1e /interp/notation.ml | |
| parent | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (diff) | |
| parent | 70d557994583bd081787e28f68d627a0833eb9c0 (diff) | |
Merge PR #13299: Remember universe instances of constants in notations
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
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 |