diff options
-rw-r--r-- | interp/notation_ops.ml | 19 | ||||
-rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 4 |
3 files changed, 16 insertions, 9 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 034116731..99e18f09e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -297,28 +297,29 @@ let compare_recursive_parts found f f' (iterator,subc) = user_err ?loc:(subtract_loc loc1 loc2) (str "Both ends of the recursive pattern are the same.") | Some (x,y,RecursiveTerms lassoc) -> - let newfound,x,y,lassoc = + let toadd,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) then - !found,x,y,lassoc + None,x,y,lassoc else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) then - !found,y,x,not lassoc + None,y,x,not lassoc else - (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in + Some (x,y),x,y,lassoc in let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in - (* found have been collected by compare_constr *) - found := newfound; + (* found variables have been collected by compare_constr *) + found := (List.remove Id.equal y (pi1 !found), + Option.fold_right (fun a l -> a::l) toadd (pi2 !found), + pi3 !found); NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,RecursiveBinders (t_x,t_y)) -> - let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in (* found have been collected by compare_constr *) - found := newfound; + found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found); check_is_hole x t_x; check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) @@ -348,7 +349,7 @@ let notation_constr_and_vars_of_glob_constr a = | _c -> aux' c and aux' x = DAst.with_val (function - | GVar id -> add_id found id; NVar id + | GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id | GApp (g,args) -> NApp (aux g, List.map aux args) | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e5dbfcb4b..65efe228a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -122,3 +122,5 @@ return (1, 2, 3, 4) : nat * nat * nat * nat {{ 1 | 1 // 1 }} : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b1015137d..ea372ad1a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4). Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. + +(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) +Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). +Check !!! (x y:nat), True. |