diff options
| author | herbelin | 2000-11-23 13:31:42 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-23 13:31:42 +0000 |
| commit | 71df2a928fb9367a632a6869306626e3a5c7a971 (patch) | |
| tree | 9c01853ae7eefff4b936a2338164476e0874b5a7 /kernel | |
| parent | 32e4b999885f34e89077c5a4d686f75b9633ad87 (diff) | |
Ajout push_rels_assum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |