diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /kernel/vm.ml | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
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 6b7a86d6f..4e13881b8 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 ")") |