summaryrefslogtreecommitdiff
path: root/test-suite/success/Print.v
blob: c4726bf3ff78bde9ec76ecd5fab43b441a8ebd37 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Print Tables.
Print ML Path.
Print ML Modules.
Print LoadPath.
Print Graph.
Print Coercions.
Print Classes.
Print nat.
Print Term O.
Print All.
Print Grammar constr.
Inspect 10.

Section A.
Coercion f (x : nat) : Prop := True.
Print Coercion Paths nat Sortclass.

Print Section A.