diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 28136e1fc..119b70e30 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -92,7 +92,7 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = Constant.t puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey type 'a infos_cache type 'a infos = { @@ -122,8 +122,8 @@ type fterm = | FAtom of constr (** Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive puniverses - | FConstruct of constructor puniverses + | FInd of inductive Univ.puniverses + | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array | FProj of projection * fconstr | FFix of fixpoint * fconstr subs |