diff options
| author | Hugo Herbelin | 2020-09-01 17:01:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 17:25:16 +0100 |
| commit | 094c395ede48f39caf7a48b663abb0e61769369e (patch) | |
| tree | d589365cf629e3ddf1a1cff1771c491921e18dbd /interp/constrextern.ml | |
| parent | 58b24bdf4393d5522df63d31b2adc9eb08c417d8 (diff) | |
Fix #9569 (notations collect the spine binding variables at printing time).
This allows to know which global references whose basename may be
unexpectedly caught need to be qualified.
Note: the alternative strategy, which is sometimes used, of renaming
the binding variables so as to avoid collisions with the basename of a
global reference is somehow less nice.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d1bec16a3f..bfeef59eaf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -85,7 +85,7 @@ let is_reserved_type na t = | Name id -> try let pat = Reserve.find_reserved_type id in - let _ = match_notation_constr false t ([],pat) in + let _ = match_notation_constr false t Id.Set.empty ([],pat) in true with Not_found | No_match -> false @@ -1273,7 +1273,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = - match_notation_constr !print_universes t pat in + match_notation_constr !print_universes t vars pat in (* Try availability of interpretation ... *) match keyrule with | NotationRule (_,ntn as specific_ntn) -> @@ -1293,20 +1293,20 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | Some (scopt,key) -> let scopes' = Option.List.cons scopt (snd scopes) in let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true (subentry,(scopt,scl@scopes')) vars c) terms in let ll = - List.map (fun (c,(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) c) + List.map (fun ((vars,l),(subentry,(scopt,scl))) -> + List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) termlists in let bl = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) binders in let bll = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in @@ -1316,7 +1316,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) terms in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in |