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 /kernel/vm.ml | |
| parent | a7df689e73dd396dafdbb4891d534b7fa5cb0fc8 (diff) | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 6b7a86d6f9..4e13881b87 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -357,7 +357,7 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = constant tableKey + type t = Constant.t tableKey let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function @@ -654,10 +654,10 @@ let apply_whd k whd = let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Names.pr_con c + | ConstKey c -> Constant.print c | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" | Atype _ -> str "Atype(") and pr_whd w = Pp.(match w with @@ -679,4 +679,4 @@ and pr_zipper z = | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") |