blob: ad69ced19eee3bd7a7b34fbc9a1741d2bc00b8e5 (
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(* The "?" of cons and eq should be inferred *)
Variable list : Set -> Set.
Variable cons : forall T : Set, T -> list T -> list T.
Check (forall n : list nat, exists l : _, (exists x : _, n = cons _ x l)).
(* Examples provided by Eduardo Gimenez *)
Definition c A (Q : (nat * A -> Prop) -> Prop) P :=
Q (fun p : nat * A => let (i, v) := p in P i v).
(* What does this test ? *)
Require Import List.
Definition list_forall_bool (A : Set) (p : A -> bool)
(l : list A) : bool :=
fold_right (fun a r => if p a then r else false) true l.
(* Checks that solvable ? in the lambda prefix of the definition are harmless*)
Parameter A1 A2 F B C : Set.
Parameter f : F -> A1 -> B.
Definition f1 frm0 a1 : B := f frm0 a1.
(* Checks that solvable ? in the type part of the definition are harmless *)
Definition f2 frm0 a1 : B := f frm0 a1.
(* Checks that sorts that are evars are handled correctly (bug 705) *)
Require Import List.
Fixpoint build (nl : list nat) :
match nl with
| nil => True
| _ => False
end -> unit :=
match nl return (match nl with
| nil => True
| _ => False
end -> unit) with
| nil => fun _ => tt
| n :: rest =>
match n with
| O => fun _ => tt
| S m => fun a => build rest (False_ind _ a)
end
end.
(* Checks that disjoint contexts are correctly set by restrict_hyp *)
(* Bug de 1999 corrigé en déc 2004 *)
Check
(let p :=
fun (m : nat) f (n : nat) =>
match f m n with
| exist a b => exist _ a b
end in
p
:forall x : nat,
(forall y n : nat, {q : nat | y = q * n}) ->
forall n : nat, {q : nat | x = q * n}).
(* Check instantiation of nested evars (bug #1089) *)
Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
Theorem contradiction : forall p, ~ p -> p -> False.
Proof. trivial. Qed.
Hint Resolve contradiction.
Goal False.
eauto.
(* This used to fail in V8.1beta because first-order unification was
used before using type information *)
Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
Check (exist _ O I : {n:nat|True}).
|
