- déplacement (encore une fois !) des variables existentielles : elles sont

   toujours dans le noyau (en ce sens que Reduction et Typeops les
   connaissent) mais dans un argument supplémentaire A COTE de l'environnement
   (de type unsafe_env)
 - Indtypes et Typing n'utilisent strictement que Evd.empty


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

1 files changed, 12 insertions, 5 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index a7ee12c3e4..f6c27a8be6 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -10,7 +10,7 @@ open Inductive
 open Environ
 open Instantiate
 open Univ
-
+open Evd
 
 let stats = ref false
 let share = ref true
@@ -136,6 +136,7 @@ type ('a, 'b) infos = {
   i_flags : flags;
   i_repr : ('a, 'b) infos -> constr -> 'a;
   i_env : unsafe_env;
+  i_evc : 'b evar_map;
   i_tab : (constr, 'a) Hashtbl.t }
 
 let const_value_cache info c =
@@ -149,8 +150,12 @@ let const_value_cache info c =
           Some v
       | None -> None
 
-let infos_under { i_flags = flg; i_repr = rfun; i_env = env; i_tab = tab } =
-  { i_flags = flags_under flg; i_repr = rfun; i_env = env; i_tab = tab }
+let infos_under infos =
+  { i_flags = flags_under infos.i_flags; 
+    i_repr = infos.i_repr; 
+    i_env = infos.i_env; 
+    i_evc = infos.i_evc;
+    i_tab = infos.i_tab }
 
 
 (**** Call by value reduction ****)
@@ -464,10 +469,11 @@ and cbv_norm_value info = function (* reduction under binders *)
 type 'a cbv_infos = (cbv_value, 'a) infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
   { i_flags = flgs;
     i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c);
     i_env = env;
+    i_evc = sigma;
     i_tab = Hashtbl.create 17 }
 
 
@@ -847,10 +853,11 @@ let search_frozen_cst info op vars =
 (* cache of constants: the body is computed only when needed. *)
 type 'a clos_infos = (fconstr, 'a) infos
 
-let create_clos_infos flgs env =
+let create_clos_infos flgs env sigma =
   { i_flags = flgs;
     i_repr = (fun old_info c -> inject c);
     i_env = env;
+    i_evc = sigma;
     i_tab = Hashtbl.create 17 }
 
 let clos_infos_env infos = infos.i_env