aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/par_abstract.v
blob: 7f6f9d6279053a6f838d544b42ac003fcef2e55a (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
Axiom T : Type.

Lemma foo : True * Type.
Proof.
  split.
  par: abstract (exact I || exact T).
Defined.

(* Yes, these names are generated hence
   the test is fragile.  I want to assert
   that abstract was correctly handled
   by par: *)
Check foo_subproof.
Check foo_subproof0.
Check (refl_equal _ :
  foo =
  pair foo_subproof foo_subproof0).

Lemma bar : True * Type.
Proof.
  split.
  par: (exact I || exact T).
Defined.
Check (refl_equal _ :
  bar = pair I T).