diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-01 13:25:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-05 17:31:04 +0200 |
| commit | cff6f53cbef53ce3902e59853f7a7dc9b7150f45 (patch) | |
| tree | 27cfa7cadd315f7784bda289756b09e86176e945 /test-suite | |
| parent | 6c92a59efd01b4fd8a11eebb01fc5d2a3db6c2ee (diff) | |
Adding a test-suite pattern-unification example that Econstr fixed.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/unification.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 296686e16..6f7498d65 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -188,3 +188,14 @@ Proof. apply idpath. apply idpath. Defined. + +(* An example where it is necessary to evar-normalize the instance of + an evar to evaluate if it is a pattern *) + +Check + let a := ?[P] in + fun (H : forall y (P : nat -> Prop), y = 0 -> P y) + x (p:x=0) => + H ?[y] a p : x = 0. +(* We have to solve "?P ?y[x] == x = 0" knowing from + "p : (x=0) == (?y[x] = 0)" that "?y := x" *) |