blob: 76511a44c5e1eaebbc39f72728cbf79c52d35c3e (
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
|
Require Import Coq.Program.Tactics.
Set Universe Polymorphism.
Obligation Tactic := idtac.
Program Definition foo : Type := _.
Program Definition bar : Type := _.
Admit Obligations.
(* Error: Anomaly "Uncaught exception AcyclicGraph.Make(Point).AlreadyDeclared."
Please report at http://coq.inria.fr/bugs/.
*)
Print foo.
Print foo_obligation_1.
Print bar.
Print bar_obligation_1.
Program Definition baz : Type := _.
Admit Obligations of baz.
Print baz.
Print baz_obligation_1.
Admit Obligations.
Fail Admit Obligations of nobody.
|
