diff options
| author | Pierre-Marie Pédrot | 2017-07-07 16:33:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-11 14:50:47 +0200 |
| commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
| tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /kernel/reduction.ml | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index de4efbba93..423e0d9349 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -680,8 +680,7 @@ let infer_check_conv_constructors let check_inductive_instances cv_pb cumi u u' univs = let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && @@ -767,8 +766,7 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && |