diff options
| -rw-r--r-- | interp/notation_ops.ml | 3 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 5 |
3 files changed, 9 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5abc7794b..ec4b2e938 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -577,7 +577,8 @@ let rec alpha_var id1 id2 = function let add_env alp (sigma,sigmalist,sigmabinders) var v = (* Check that no capture of binding variables occur *) - if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; + if not (Id.equal ldots_var var) && + List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match; (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::sigma,sigmalist,sigmabinders) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 6ff1d3837..13ed7816d 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -54,3 +54,5 @@ end : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0} exist (Q x) y conj : {x0 : A | Q x x0} +{1, 2} + : nat -> Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4e0d135d7..3f3945052 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -106,3 +106,8 @@ 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). + +(* Check bug raised on coq-club on Sep 12, 2016 *) + +Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))). +Check ({1, 2}). |