diff options
| author | Maxime Dénès | 2018-03-04 16:46:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:46:49 +0100 |
| commit | 9cd987a07d3792dc200e15c5e792a25a1a99c9c6 (patch) | |
| tree | efa4cbcd3d3959485e8a2f7b4bbb1d5888603be4 /kernel/vmvalues.mli | |
| parent | 0a9a45abbd3421f3b2cfc4f6428938898a933ffe (diff) | |
| parent | c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 (diff) | |
Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort
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 350f71372f..570e3606ae 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -57,7 +57,7 @@ val cofix_upd_code : to_update -> tcode type atom = | Aid of Vars.id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -70,7 +70,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option |