aboutsummaryrefslogtreecommitdiff
path: root/kernel/context.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/context.mli')
-rw-r--r--kernel/context.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/context.mli b/kernel/context.mli
index 091d701a28..955e214cb9 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -260,6 +260,7 @@ sig
| LocalDef of Id.t list * Constr.t * Constr.t
val map_constr : (Constr.t -> Constr.t) -> t -> t
+ val of_named_decl : Named.Declaration.t -> t
val to_named_context : t -> Named.t
end