blob: 49b16f62546a82813724c9a36d1ba1e442d33efd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
(* A slight shortening of bug 6078 *)
(* This bug exposed a different behavior of unshelve_unifiable
depending on which projection is found in the unification
heuristics *)
Axiom flat_type : Type.
Axiom interp_flat_type : flat_type -> Type.
Inductive type := Arrow (_ _ : flat_type).
Definition interp_type (t : type)
:= interp_flat_type (match t with Arrow s d => s end)
-> interp_flat_type (match t with Arrow s d => d end).
Axiom Expr : type -> Type.
Axiom Interp : forall {t : type}, Expr t -> interp_type t.
Axiom Wf : forall {t}, Expr t -> Prop.
Axiom a : forall f, interp_flat_type f.
Definition packaged_expr_functionP A :=
(fun F : Expr A -> Expr A
=> forall e' v, Interp (F e') v = a (let (_,f) := A in f)).
Goal forall (f f0 : flat_type)
(e : forall _ : Expr (@Arrow f f0),
Expr (@Arrow f f0)),
@packaged_expr_functionP (@Arrow f f0) e.
intros.
refine (fun (e0 : Expr (Arrow f f0))
=> (fun zHwf':True =>
(fun v : interp_flat_type f =>
?[G] : ?[U] = ?[V] :> interp_flat_type ?[v])) ?[H]);
[ | ].
(* Was: Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *)
Abort.
|
