diff options
author | 2016-07-16 16:24:59 +0200 | |
---|---|---|
committer | 2016-10-12 16:07:56 +0200 | |
commit | 5dd690ee5975262d34d8dcc44191138c8d326f65 (patch) | |
tree | c54f5fb3f8cfee72b8ee640bff2df37957b921d2 | |
parent | d48176857632e1d2a0af0a31dc922f3c52047707 (diff) |
Fixing a collision about the meta-variable ".." in recursive notations.
This happens when recursive notations are used to define recursive
notations.
-rw-r--r-- | interp/constrintern.ml | 20 | ||||
-rw-r--r-- | test-suite/success/Notations.v | 3 |
2 files changed, 11 insertions, 12 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f30d3cefa..478adf011 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -517,27 +517,24 @@ let rec subordinate_letins letins = function | [] -> letins,[] -let rec subst_iterator y t = function - | GVar (_,id) as x -> if Id.equal id y then t else x - | x -> map_glob_constr (subst_iterator y t) x - let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in - let rec aux (terms,binderopt as subst') (renaming,env) c = + let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with + | NVar id when Id.equal id ldots_var -> Option.get terminopt | NVar id -> subst_var subst' (renaming, env) id | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x termlists in - let termin = aux subst' subinfos terminator in + let termin = aux (terms,None,None) subinfos terminator in let fold a t = let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in - subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter) + aux (nterms,None,Some t) subinfos iter in List.fold_right fold (if lassoc then List.rev l else l) termin with Not_found -> @@ -582,10 +579,9 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in let letins,bl = subordinate_letins [] bl in - let termin = aux subst' (renaming,env) terminator in + let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> - subst_iterator ldots_var t - (aux (terms,Some(x,binder)) subinfos iter)) + aux (terms,Some(x,binder),Some t) subinfos iter) termin bl in make_letins letins res with Not_found -> @@ -610,7 +606,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = | t -> glob_constr_of_notation_constr_with_binders loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, binderopt) (renaming, env) id = + and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -623,7 +619,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) GVar (loc,id) - in aux (terms,None) infos c + in aux (terms,None,None) infos c let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index b72a06740..2f7c62972 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l). Notation "'intros' x" := (S x) (at level 0). Goal True -> True. intros H. exact H. Qed. + +(* Check absence of collision on ".." in nested notations with ".." *) +Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). |