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/cooking.ml | |
| parent | a7df689e73dd396dafdbb4891d534b7fa5cb0fc8 (diff) | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 80d41847cd..08fff0ca41 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -29,15 +29,15 @@ let pop_dirpath p = match DirPath.repr p with | _::l -> DirPath.make l let pop_mind kn = - let (mp,dir,l) = Names.repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_con con = - let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l type my_global_reference = - | ConstRef of constant + | ConstRef of Constant.t | IndRef of inductive | ConstructRef of constructor |