diff options
| author | herbelin | 2000-10-11 20:04:04 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-11 20:04:04 +0000 |
| commit | d6bcb300547267487db417e57c2f745f4fb31cbb (patch) | |
| tree | 19c85e6310568578ade8ce82e8a8b8b4818294d8 /kernel | |
| parent | 6617dfae5110021b28e565fb3ea5b0d58fb9c14a (diff) | |
Ajout push_rec_types
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 41be8a6796..bce436ade1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -116,6 +116,12 @@ let push_rels_to_vars env = env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0) in subst, (var_context_app (fun _ -> sign) env) +let push_rec_types (typarray,names,_) env = + let vect_lift_type = Array.mapi (fun i t -> outcast_type (lift i t)) in + let nlara = + List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in + List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara + let reset_rel_context env = { env with env_context = { env_var_context = env.env_context.env_var_context; diff --git a/kernel/environ.mli b/kernel/environ.mli index 6327c735b4..30d93a02e4 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -48,6 +48,9 @@ val names_of_rel_context : env -> names_context (*s Returns also the substitution to be applied to rel's *) val push_rels_to_vars : env -> constr list * env +(*s Push the types of a (co-)fixpoint *) +val push_rec_types : rec_declaration -> env -> env + (* Gives identifiers in [var_context] and [rel_context] *) val ids_of_context : env -> identifier list val map_context : (constr -> constr) -> env -> env |