aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cClosure.ml')
-rw-r--r--kernel/cClosure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1d5142a5c..61ed40394 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -265,7 +265,7 @@ type 'a infos_cache = {
i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
- i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t;
+ i_rels : (Constr.rel_declaration * lazy_val) Range.t;
}
and 'a infos = {