Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in

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

3 files changed, 15 insertions, 26 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3b27a32b3..b44077234 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -75,16 +75,6 @@ let rec map_append_vect f v =
 
 
 
-(* behaves as lam_and_popl but receives an environment instead of a 
- *  dbenvironment
- *)
-let elam_and_popl n env body =
-  let ENVIRON(sign,dbenv)=env  in
-  let ndbenv,a,l = lam_and_popl n dbenv body []
-  in ENVIRON(sign,ndbenv),a
-
-
-
 (* behaves as lam_and_popl_named but receives an environment instead of a 
  *  dbenvironment
  *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d4dd1da18..60b16fc9f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -311,7 +311,7 @@ let rec detype avoid env t =
 	 | Name id   -> RRef (dummy_loc, RVar id)
 	 | Anonymous -> anomaly "detype: index to an anonymous variable"
        with Not_found ->
-	 let s = "[REL "^(string_of_int (n - List.length (get_rels env)))^"]"
+	 let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
 	 in RRef (dummy_loc, RVar (id_of_string s)))
     | IsMeta n -> RRef (dummy_loc,RMeta n)
     | IsVar id -> RRef (dummy_loc,RVar id)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2f0757412..11e759aee 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -201,23 +201,22 @@ let real_clean isevars sp args rhs =
 (* [new_isevar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 
+let append_rels_to_vars ctxt =
+  dbenv_it
+    (fun na t (subst,sign) ->
+       let na = if na = Anonymous then Name(id_of_string"_") else na in
+       let id = next_name_away na (ids_of_sign sign) in
+       ((VAR id)::subst, add_sign (id,typed_app (substl subst) t) sign))
+    ctxt ([],get_globals ctxt)
+
 let new_isevar isevars env typ k =
-  let (ENVIRON(sign,dbenv)) = context env in
-  let t =
-    List.fold_left (fun b (na,d)-> mkLambda na (incast_type d) b) typ dbenv in
-  let rec aux sign = function
-    | (0, t) -> (sign,t)
-    | (n, DOP2(Lambda,d,(DLAM(na,b)))) ->
-	let na = if na = Anonymous then Name(id_of_string"_") else na in
-       	let id = next_name_away na (ids_of_sign sign) in
-       	aux (add_sign (id,(outcast_type d)) sign) (n-1, subst1 (VAR id) b)
-    | (_, _) -> anomaly "Trad.new_isevar" 
-  in
-  let (sign',typ') = aux sign (List.length dbenv, t) in
-  let env' = change_hyps (fun _ -> sign') env in
+  let ctxt = context env in
+  let subst,sign = append_rels_to_vars ctxt in
+  let typ' = substl subst typ in
+  let env' = change_hyps (fun _ -> sign) env in
   let newargs =
-    (List.rev(rel_list 0 (List.length dbenv)))
-    @(List.map (fun id -> VAR id) (ids_of_sign sign)) in
+    (List.rev(rel_list 0 (number_of_rels ctxt)))
+    @(List.map (fun id -> VAR id) (ids_of_sign (get_globals ctxt))) in
   let (sigma',evar) =
     new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
   isevars := sigma';