aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-10 18:05:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 14:50:47 +0200
commitb8a7222e670f69e024d50394afd88204e15d1b29 (patch)
tree90c3c75ca9c2647ad41c6a30954cdf8ce3f6b5d8 /engine/universes.ml
parent1309723672def9bf322a23e9c789e4a8bc2a4ac3 (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 'engine/universes.ml')
-rw-r--r--engine/universes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/universes.ml b/engine/universes.ml
index 5df02c8a9..fc441fd0b 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -287,7 +287,7 @@ let fresh_universe_instance ctx =
let fresh_instance_from_context ctx =
let inst = fresh_universe_instance ctx in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, constraints
let fresh_instance ctx =
@@ -316,7 +316,7 @@ let fresh_instance_from ctx inst =
| Some inst -> existing_instance ctx inst
| None -> fresh_instance ctx
in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, (ctx', constraints)
let unsafe_instance_from ctx =