diff options
| author | Gregory Malecha | 2015-11-09 16:22:18 -0800 |
|---|---|---|
| committer | Maxime Dénès | 2015-12-09 14:25:56 +0100 |
| commit | 8e7803224eeb32e83600905c2c855e32e7bf8ffb (patch) | |
| tree | 39090b309bc28f3bd2d9b59b62c43c9b656510a0 /kernel/vm.mli | |
| parent | 11eedd379d4b27e73a1999c0aacc2056311e8ba9 (diff) | |
bug fixes to vm computation + test cases.
Diffstat (limited to 'kernel/vm.mli')
| -rw-r--r-- | kernel/vm.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli index 43a42eb9c4..6e9579aa46 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -48,8 +48,11 @@ type whd = | Vatom_stk of atom * stack | Vuniv_level of Univ.universe_level +(** For debugging purposes only *) + val pr_atom : atom -> Pp.std_ppcmds val pr_whd : whd -> Pp.std_ppcmds +val pr_stack : stack -> Pp.std_ppcmds (** Constructors *) |