aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
commit2ca003899ea4a24a470c32dc186b95ef3de3ca19 (patch)
treee7444295b47223d16db6db5beafde4839a0cf926 /kernel/environ.ml
parentacbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff)
parent21ed95122a088cab6808200778719270d9cc9078 (diff)
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r--kernel/environ.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 224b6d5b8..4ab469803 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -77,13 +77,13 @@ let dummy_lazy_val () = ref VKnone
let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
type named_context_val = {
- env_named_ctx : Context.Named.t;
- env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+ env_named_ctx : Constr.named_context;
+ env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
}
type rel_context_val = {
- env_rel_ctx : Context.Rel.t;
- env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+ env_rel_ctx : Constr.rel_context;
+ env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
}
type env = {