From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- kernel/cClosure.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 7e193ef82..e8cce0841 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -85,7 +85,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds @@ -114,7 +114,7 @@ module RedFlags = (struct type red_kind = BETA | DELTA | ETA | MATCH | FIX | COFIX | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA @@ -234,7 +234,7 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' @@ -401,7 +401,7 @@ let update v1 no t = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr -- cgit v1.2.3