Ajout push_rec_types

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 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;