diff options
| author | herbelin | 2001-05-25 06:22:08 +0000 |
|---|---|---|
| committer | herbelin | 2001-05-25 06:22:08 +0000 |
| commit | e6ba2e83fe0cb5e2fc53844bd0f5fe4b6d8ffb97 (patch) | |
| tree | cd8129b18ea71d58dde99ae1aeb9d01bcd6295fd /kernel/environ.mli | |
| parent | dc2e676c9cdedea43805c21a4b3203832a985f95 (diff) | |
Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1762 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index adbbf0c5ce..ca93b84e78 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -54,9 +54,12 @@ val names_of_rel_context : env -> names_context (*s Returns also the substitution to be applied to rel's *) val push_rel_context_to_named_context : env -> constr list * env -(*s Push the types of a (co-)fixpoint *) +(*s Push the types of a (co-)fixpoint to [rel_context] *) val push_rec_types : rec_declaration -> env -> env +(*s Push the types of a (co-)fixpoint to [named_context] *) +val push_named_rec_types : rec_declaration -> env -> env + (* Gives identifiers in [named_context] and [rel_context] *) val ids_of_context : env -> identifier list val map_context : (constr -> constr) -> env -> env |