blob: 0be859eddffa55676edbd21e928fd95538996929 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Dependent higher-order hole in "refine" (simplified version) *)
Set Implicit Arguments.
Inductive Nest t := Cons : Nest (prod t t) -> Nest t.
Definition cast A x y Heq P H := @eq_rect A x P H y Heq.
Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta.
It raises a regular error in 8.3 and almost succeeds with the new
proof engine: there are two solutions to a unification problem
(P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
leave P as subgoal or choose itself one solution *)
intros. refine (Cons (cast H _ y)).
|
