diff options
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 8f39cfae4..86debd5d5 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -65,7 +65,7 @@ val eq_id_key : id_key -> id_key -> bool type atom = | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -78,7 +78,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option |