diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 18:54:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 20:30:11 +0200 |
| commit | 5d3d60e88f137183b4155bfa446dc7f3ebb35993 (patch) | |
| tree | 47b14bce769ce243310173d8abf8033619d34592 /interp/notation_ops.ml | |
| parent | a267b06c4a237ce3e4ce257e47f6429543804baa (diff) | |
Fixing a bug of recursive notations introduced in dfdaf4de.
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 19 |
1 files changed, 10 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) |