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
|
(* Test that it raises a normal error and not an anomaly *)
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Arguments fst {A B} _.
Arguments snd {A B} _.
Arguments pair {A B} _ _.
Record piis := { dep_types : Type; indep_args : dep_types -> Type }.
Import EqNotations.
Goal forall (id : Set) (V : id) (piiio : id -> piis)
(Z : {ridc : id & prod (dep_types (piiio ridc)) True})
(P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}),
let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in
prod True (ida V (projT1 W)) ->
Z = existT _ V (pair (projT1 W) I) ->
ida (projT1 Z) (fst (projT2 Z)).
intros.
refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
H in
let v := I in
_);
refine (snd X).
Undo.
Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
H in
let v := I in
snd X).
Abort.
|
