diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ed74f0f2d8..17b411f9f7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -101,6 +101,9 @@ let push_rel d = rel_context_app (add_rel_decl d) let push_rel_def def = rel_context_app (add_rel_def def) let push_rel_assum decl = rel_context_app (add_rel_assum decl) let push_rels ctxt = rel_context_app (concat_rel_context ctxt) +let push_rels_assum decl env = + rel_context_app (List.fold_right add_rel_assum decl) env + let push_rel_context_to_named_context env = let sign0 = env.env_context.env_named_context in @@ -395,3 +398,4 @@ type unsafe_judgment = { type unsafe_type_judgment = { utj_val : constr; utj_type : sorts } + diff --git a/kernel/environ.mli b/kernel/environ.mli index 7e90dd4cd0..c0a0dcc9a7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -41,6 +41,7 @@ val push_rel : rel_declaration -> env -> env val push_rel_assum : name * types -> env -> env val push_rel_def : name * constr * types -> env -> env val push_rels : rel_context -> env -> env +val push_rels_assum : (name * types) list -> env -> env val names_of_rel_context : env -> names_context (*s Returns also the substitution to be applied to rel's *) |