blob: 7fae32871584d956716cf1b373e872d255339cf2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* 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. Fail refine (Cons (cast H _ y)).
Unset Solve Unification Constraints. (* Keep the unification constraint around *)
refine (Cons (cast H _ y)).
intros.
refine (Nest (prod X X)). Qed.
|
