diff options
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r-- | interp/notation_ops.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6561000c4..5ceb25a8f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -854,15 +854,21 @@ let rec match_ inner u alp metas sigma a1 a2 = otherwise how to ensure it corresponds to a well-typed eta-expansion; we make an exception for types which are metavariables: this is useful e.g. to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) - | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner -> - let id' = Namegen.next_ident_away id (free_glob_vars b1) in + | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> + let avoid = + free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in + let id' = Namegen.next_ident_away id avoid in let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 | _ -> assert false in - match_in u alp metas (add_bindinglist_env sigma id [(Name id',Explicit,None,t1)]) - (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 + let (alp,sigma) = + if is_bindinglist_meta id metas then + alp, add_bindinglist_env sigma id [(Name id',Explicit,None,t1)] + else + match_names metas (alp,sigma) (Name id') na in + match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match |