diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 274d3655d3..07160dcf6f 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -71,10 +71,10 @@ let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type" let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev" let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) - | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) - | NList (_,_,NApp (NRef ref,args),_,_) - | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) - | NRef ref -> RefKey(canonical_gr ref), None + | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), Some (List.length args) + | NList (_,_,NApp (NRef (ref,_),args),_,_) + | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) + | NRef (ref,_) -> RefKey(canonical_gr ref), None | _ -> Oth, None let cache_reserved_type (_,(id,t)) = |