diff options
| author | Maxime Dénès | 2017-11-13 11:22:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:22:41 +0100 |
| commit | b75f803afb3189a9f3b594a190fdb8d6207e7624 (patch) | |
| tree | 28b33d0d1ffa2fbe42d044235987f34b0c733fbb /checker/closure.ml | |
| parent | a7df689e73dd396dafdbb4891d534b7fa5cb0fc8 (diff) | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 70718bfdca..7982ffa7a5 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -63,7 +63,7 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : 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 @@ -86,7 +86,7 @@ module RedFlags = (struct r_iota : bool } type red_kind = BETA | DELTA | IOTA | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fIOTA = IOTA @@ -165,7 +165,7 @@ type 'a tableKey = | VarKey of Id.t | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey module KeyHash = struct @@ -281,9 +281,9 @@ and fterm = | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *) | FLIFT of int * fconstr | FCLOS of constr * fconstr subs |