diff options
Diffstat (limited to 'test-suite/success/unification.v')
| -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" *) |