diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 18:05:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | b8a7222e670f69e024d50394afd88204e15d1b29 (patch) | |
| tree | 90c3c75ca9c2647ad41c6a30954cdf8ce3f6b5d8 /pretyping | |
| parent | 1309723672def9bf322a23e9c789e4a8bc2a4ac3 (diff) | |
Less footguns in universe handling: remove subst_instance_context.
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
2 files changed, 3 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2acf6bfe6..87f29ba49 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -363,9 +363,7 @@ let check_leq_inductives evd cumi u u' = else begin let comp_subst = (Univ.Instance.append u u') in - let comp_cst = - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) - in + let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in Evd.add_constraints evd comp_cst end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3acefa134..21ed8e0a2 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1372,15 +1372,13 @@ let sigma_check_inductive_instances cv_pb uinfind u u' sigma = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) + Univ.AUContext.instantiate comp_subst ind_sbctx in let comp_cst = match cv_pb with Reduction.CONV -> let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = - Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) - in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in |