aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 45812b5a1..9bf743152 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1209,3 +1209,10 @@ let hcons =
Id.hcons)
(* let hcons_types = hcons_constr *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list