From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Jul 2017 16:33:47 +0200 Subject: 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. --- pretyping/reductionops.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index cc1709f1c..3acefa134 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1362,12 +1362,12 @@ let sigma_compare_instances ~flex i0 i1 sigma = raise Reduction.NotConvertible let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) in let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + if not ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = -- cgit v1.2.3