diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 14 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 12 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 1 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 8 |
6 files changed, 41 insertions, 5 deletions
@@ -1,3 +1,10 @@ +Changes from V8.5pl1 to V8.5pl2 +=============================== + +Bugfixes + +- #4677: fix alpha-conversion in notations needing eta-expansion + Changes from V8.5 to V8.5pl1 ============================ diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 51dfadac0..5abc7794b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -794,15 +794,21 @@ let rec match_ inner u alp (tmetas,blmetas as 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_env alp sigma id2 t1 | _ -> assert false in - match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,t1)]) - (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 + let (alp,sigma) = + if Id.List.mem id blmetas then + alp, bind_binder 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 diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index c9860864a..e3b6fb08a 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -266,7 +266,7 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Id.Set.add id set -let free_glob_vars = +let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) @@ -324,6 +324,16 @@ let free_glob_vars = let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs +let glob_visible_short_qualid c = + let rec aux acc = function + | GRef (_,c,_) -> + let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in + let dir,id = Libnames.repr_qualid qualid in + if DirPath.is_empty dir then id :: acc else acc + | c -> + fold_glob_constr aux acc c + in aux [] c + let add_and_check_ident id set = if Id.Set.mem id set then Pp.(msg_warning diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 45444234a..e0a2de032 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -40,6 +40,7 @@ val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t +val glob_visible_short_qualid : glob_constr -> Id.t list (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 58ec1de56..6ff1d3837 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -50,3 +50,7 @@ end : nat -> nat # _ : nat => 2 : nat -> nat +# x : nat => # H : x <= 0 => exist (le x) 0 H + : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0} +exist (Q x) y conj + : {x0 : A | Q x x0} diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index e53c94ef0..c9efe1ead 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -68,8 +68,10 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* In practice, only the printing rule is used here *) (* Note: does not work for pattern *) +Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). Check fun f x => f x + S x. +End A. Open Scope list_scope. Notation list1 := (1::nil)%list. @@ -98,3 +100,9 @@ Notation "# x : T => t" := (fun x : T => t) Check # x : nat => x. Check # _ : nat => 2. + +(* Check bug 4677 *) +Check fun x (H:le x 0) => exist (le x) 0 H. + +Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). +Check (exist (Q x) y conj). |