les variables existentielles contiennent maintenant un environnement (type

unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres
le module Environ.


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

5 files changed, 18 insertions, 6 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 004ef8e536..a983a67597 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -50,6 +50,10 @@ let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 let push_var idvar env =
   { env with env_context = add_glob idvar env.env_context }
 
+let change_hyps f env =
+  let ctx = env.env_context in
+  { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) }
+
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 61fb4b64a6..d3fd22c01e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -4,7 +4,6 @@
 (*i*)
 open Names
 open Term
-open Evd
 open Constant
 open Inductive
 open Abstraction
@@ -25,7 +24,11 @@ val universes : unsafe_env -> universes
 val context : unsafe_env -> context
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
+val change_hyps : 
+  (typed_type signature -> typed_type signature) -> unsafe_env -> unsafe_env
+
 val push_rel : name * typed_type -> unsafe_env -> unsafe_env
+
 val set_universes : universes -> unsafe_env -> unsafe_env
 val add_constraints : constraints -> unsafe_env -> unsafe_env
 val add_constant : 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 270ad1f2e4..b31f2f6b79 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -5,6 +5,7 @@ open Util
 open Names
 open Term
 open Sign
+open Environ
 
 (* The type of mappings for existential variables *)
 
@@ -20,7 +21,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_hyps : typed_type signature;
+  evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
 
@@ -41,7 +42,7 @@ let define evd ev body =
   let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_hyps = oldinfo.evar_hyps;
+      evar_env = oldinfo.evar_env;
       evar_body = Evar_defined body;
       evar_info = oldinfo.evar_info } 
   in
@@ -66,3 +67,4 @@ let is_defined sigma ev =
 
 let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
 
+let evar_hyps ev = get_globals (context ev.evar_env)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 80e767fa85..df80ee72b7 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -5,6 +5,7 @@
 open Names
 open Term
 open Sign
+open Environ
 (*i*)
 
 (* The type of mappings for existential variables.
@@ -23,7 +24,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_hyps : typed_type signature;
+  evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
 
@@ -48,3 +49,5 @@ val is_evar : 'a evar_map -> evar -> bool
 val is_defined : 'a evar_map -> evar -> bool
 
 val metamap : 'a evar_map -> (int * constr) list
+
+val evar_hyps : 'a evar_info -> typed_type signature
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index acc48bcb05..0cdc50c562 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -71,13 +71,13 @@ let name_of_existential n = id_of_string ("?" ^ string_of_int n)
 let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
+  let hyps = evar_hyps info in
   instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
 
 let existential_value sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
+  let hyps = evar_hyps info in
   match info.evar_body with
     | Evar_defined c ->
 	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)