aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.ml')
-rw-r--r--checker/term.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/term.ml b/checker/term.ml
index b52f08cfa..a3c9225f5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -209,6 +209,9 @@ let subst1 lam = substl [lam]
(* Type of assumptions and contexts *)
(***************************************************************************)
+type named_declaration = Id.t * constr option * constr
+type named_context = named_declaration list
+
let empty_named_context = []
let fold_named_context f l ~init = List.fold_right f l init