Unify pre_env and env

We now have only two notions of environments in the kernel: env and
safe_env.

34 files changed, 416 insertions, 545 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cb1abc4a9..3321c2931 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -230,7 +230,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f1530b2d1..6810626ad 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -783,7 +783,7 @@ let of_existential : Constr.existential -> existential =
 
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
-let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e)
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 38ceed569..afedfe180 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Term
 open Constr
-open Pre_env
 open Environ
 open Evd
 open Termops
diff --git a/engine/termops.ml b/engine/termops.ml
index 053fcc3db..04fdad670 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1374,7 +1374,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
+  try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false
 
 let map_rel_decl f = function
 | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 435cf0a79..4da5f0f38 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -265,7 +265,7 @@ type 'a infos_cache = {
   i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
   i_env : env;
   i_sigma : existential -> constr option;
-  i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
+  i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t;
 }
 
 and 'a infos = {
@@ -314,12 +314,11 @@ let evar_value cache ev =
   cache.i_sigma ev
 
 let create mk_cl flgs env evars =
-  let open Pre_env in
   let cache =
     { i_repr = mk_cl;
       i_env = env;
       i_sigma = evars;
-      i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
+      i_rels = env.env_rel_context.env_rel_map;
     }
   in { i_flags = flgs; i_cache = cache }
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5f6d2d0ee..df5b17da3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -20,7 +20,7 @@ open Cinstr
 open Clambda
 open Constr
 open Declarations
-open Pre_env
+open Environ
 
 
 (* Compilation of variables + computing free variables                    *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 1c4cdcbeb..57d3e6fc2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -12,7 +12,7 @@ open Cbytecodes
 open Cemitcodes
 open Constr
 open Declarations
-open Pre_env
+open Environ
 
 (** Should only be used for monomorphic terms *)
 val compile : fail_on_error:bool ->
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 0727eaeac..619dd608f 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -6,7 +6,7 @@ open Constr
 open Declarations
 open Cbytecodes
 open Cinstr
-open Pre_env
+open Environ
 open Pp
 
 let pr_con sp = str(Names.Label.to_string (Constant.label sp))
diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 6cf46163e..8ff10b454 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -1,13 +1,14 @@
 open Names
 open Cinstr
+open Environ
 
 exception TooLargeInductive of Pp.t
 
-val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda
+val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
 
 val decompose_Llam : lambda -> Name.t array * lambda
 
-val get_alias : Pre_env.env -> Constant.t -> Constant.t
+val get_alias : env -> Constant.t -> Constant.t
 
 val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 4f3cbf289..9bacdb65f 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -20,7 +20,7 @@ open Vmvalues
 open Cemitcodes
 open Cbytecodes
 open Declarations
-open Pre_env
+open Environ
 open Cbytegen
 
 module NamedDecl = Context.Named.Declaration
@@ -142,23 +142,23 @@ and slot_for_fv env fv =
       | None -> v_of_id id, Id.Set.empty
       | Some c ->
           val_of_constr (env_of_id id env) c,
-          Environ.global_vars_set (Environ.env_of_pre_env env) c in
+          Environ.global_vars_set env c in
     build_lazy_val cache (v, d); v in
   let val_of_rel i = val_of_rel (nb_rel env - i) in
   let idfun _ x = x in
   match fv with
   | FVnamed id ->
-      let nv = Pre_env.lookup_named_val id env in
+      let nv = lookup_named_val id env in
       begin match force_lazy_val nv with
       | None ->
-	 env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
+         env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
-      let rv = Pre_env.lookup_rel_val i env in
+      let rv = lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-        env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
+        env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVevar evk -> val_of_evar evk
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index d32cfba36..72c96b0b9 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -12,7 +12,7 @@
 
 open Names
 open Constr
-open Pre_env
+open Environ
 
 val val_of_constr : env -> constr -> Vmvalues.values
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9d4063e43..c3e7cec75 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -28,26 +28,204 @@ open Names
 open Constr
 open Vars
 open Declarations
-open Pre_env
 open Context.Rel.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 (* The type of environments. *)
 
-type named_context_val = Pre_env.named_context_val
+(* The key attached to each constant is used by the VM to retrieve previous *)
+(* evaluations of the constant. It is essentially an index in the symbols table *)
+(* used by the VM. *)
+type key = int CEphemeron.key option ref
+
+(** Linking information for the native compiler. *)
+
+type link_info =
+  | Linked of string
+  | LinkedInteractive of string
+  | NotLinked
+
+type constant_key = constant_body * (link_info ref * key)
+
+type mind_key = mutual_inductive_body * link_info ref
+
+type globals = {
+  env_constants : constant_key Cmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
+  env_modules : module_body MPmap.t;
+  env_modtypes : module_type_body MPmap.t}
+
+type stratification = {
+  env_universes : UGraph.t;
+  env_engagement : engagement
+}
+
+type val_kind =
+    | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key
+    | VKnone
+
+type lazy_val = val_kind ref
+
+let force_lazy_val vk = match !vk with
+| VKnone -> None
+| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None
+
+let dummy_lazy_val () = ref VKnone
+let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
+
+type named_context_val = {
+  env_named_ctx : Context.Named.t;
+  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+}
+
+type rel_context_val = {
+  env_rel_ctx : Context.Rel.t;
+  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+}
+
+type env = {
+  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_named_context : named_context_val; (* section variables *)
+  env_rel_context   : rel_context_val;
+  env_nb_rel        : int;
+  env_stratification : stratification;
+  env_typing_flags  : typing_flags;
+  retroknowledge : Retroknowledge.retroknowledge;
+  indirect_pterms : Opaqueproof.opaquetab;
+}
+
+let empty_named_context_val = {
+  env_named_ctx = [];
+  env_named_map = Id.Map.empty;
+}
+
+let empty_rel_context_val = {
+  env_rel_ctx = [];
+  env_rel_map = Range.empty;
+}
+
+let empty_env = {
+  env_globals = {
+    env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
+    env_modules = MPmap.empty;
+    env_modtypes = MPmap.empty};
+  env_named_context = empty_named_context_val;
+  env_rel_context = empty_rel_context_val;
+  env_nb_rel = 0;
+  env_stratification = {
+    env_universes = UGraph.initial_universes;
+    env_engagement = PredicativeSet };
+  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
+  retroknowledge = Retroknowledge.initial_retroknowledge;
+  indirect_pterms = Opaqueproof.empty_opaquetab }
+
+
+(* Rel context *)
+
+let push_rel_context_val d ctx = {
+  env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx;
+  env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map;
+}
+
+let match_rel_context_val ctx = match ctx.env_rel_ctx with
+| [] -> None
+| decl :: rem ->
+  let (_, lval) = Range.hd ctx.env_rel_map in
+  let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in
+  Some (decl, lval, ctx)
+
+let push_rel d env =
+    { env with
+      env_rel_context = push_rel_context_val d env.env_rel_context;
+      env_nb_rel = env.env_nb_rel + 1 }
+
+let lookup_rel n env =
+  try fst (Range.get env.env_rel_context.env_rel_map (n - 1))
+  with Invalid_argument _ -> raise Not_found
+
+let lookup_rel_val n env =
+  try snd (Range.get env.env_rel_context.env_rel_map (n - 1))
+  with Invalid_argument _ -> raise Not_found
+
+let rel_skipn n ctx = {
+  env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx;
+  env_rel_map = Range.skipn n ctx.env_rel_map;
+}
+
+let env_of_rel n env =
+  { env with
+    env_rel_context = rel_skipn n env.env_rel_context;
+    env_nb_rel = env.env_nb_rel - n
+  }
+
+(* Named context *)
+
+let push_named_context_val_val d rval ctxt =
+(*   assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
+  {
+    env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
+    env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
+  }
+
+let push_named_context_val d ctxt =
+  push_named_context_val_val d (ref VKnone) ctxt
+
+let match_named_context_val c = match c.env_named_ctx with
+| [] -> None
+| decl :: ctx ->
+  let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
+  let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
+  let cval = { env_named_ctx = ctx; env_named_map = map } in
+  Some (decl, v, cval)
+
+let map_named_val f ctxt =
+  let open Context.Named.Declaration in
+  let fold accu d =
+    let d' = map_constr f d in
+    let accu =
+      if d == d' then accu
+      else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu
+    in
+    (accu, d')
+  in
+  let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
+  if map == ctxt.env_named_map then ctxt
+  else { env_named_ctx = ctx; env_named_map = map }
+
+let push_named d env =
+  {env with env_named_context = push_named_context_val d env.env_named_context}
+
+let lookup_named id env =
+  fst (Id.Map.find id env.env_named_context.env_named_map)
+
+let lookup_named_val id env =
+  snd(Id.Map.find id env.env_named_context.env_named_map)
+
+let lookup_named_ctxt id ctxt =
+  fst (Id.Map.find id ctxt.env_named_map)
+
+(* Global constants *)
 
-type env = Pre_env.env
+let lookup_constant_key kn env =
+  Cmap_env.find kn env.env_globals.env_constants
+
+let lookup_constant kn env =
+  fst (Cmap_env.find kn env.env_globals.env_constants)
+
+(* Mutual Inductives *)
+let lookup_mind kn env =
+  fst (Mindmap_env.find kn env.env_globals.env_inductives)
+
+let lookup_mind_key kn env =
+  Mindmap_env.find kn env.env_globals.env_inductives
 
-let pre_env env = env
-let env_of_pre_env env = env
 let oracle env = env.env_typing_flags.conv_oracle
 let set_oracle env o =
   let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in
   { env with env_typing_flags }
 
-let empty_named_context_val = empty_named_context_val
-
-let empty_env = empty_env
-
 let engagement env = env.env_stratification.env_engagement
 let typing_flags env = env.env_typing_flags
 
@@ -72,15 +250,11 @@ let empty_context env =
   | _ -> false
 
 (* Rel context *)
-let lookup_rel = lookup_rel
-
 let evaluable_rel n env =
   is_local_def (lookup_rel n env)
 
 let nb_rel env = env.env_nb_rel
 
-let push_rel = push_rel
-
 let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
@@ -105,24 +279,14 @@ let named_context_of_val c = c.env_named_ctx
 
 let ids_of_named_context_val c = Id.Map.domain c.env_named_map
 
-(* [map_named_val f ctxt] apply [f] to the body and the type of
-   each declarations.
-   *** /!\ ***   [f t] should be convertible with t *)
-let map_named_val = map_named_val
-
 let empty_named_context = Context.Named.empty
 
-let push_named = push_named
 let push_named_context = List.fold_right push_named
-let push_named_context_val = push_named_context_val
 
 let val_of_named_context ctxt =
   List.fold_right push_named_context_val ctxt empty_named_context_val
 
 
-let lookup_named = lookup_named
-let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map)
-
 let eq_named_context_val c1 c2 =
    c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2)
 
@@ -181,7 +345,10 @@ let map_universes f env =
   let s = env.env_stratification in
     { env with env_stratification =
 	 { s with env_universes = f s.env_universes } }
-				     
+
+let set_universes env u =
+  { env with env_stratification = { env.env_stratification with env_universes = u } }
+
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
   else map_universes (UGraph.merge_constraints c) env
@@ -221,8 +388,6 @@ let set_typing_flags c env = (* Unsafe *)
 
 (* Global constants *)
 
-let lookup_constant = lookup_constant
-
 let no_link_info = NotLinked
 
 let add_constant_key kn cb linkinfo env =
@@ -330,8 +495,6 @@ let is_projection cst env =
   | None -> false
 
 (* Mutual Inductives *)
-let lookup_mind = lookup_mind
-
 let polymorphic_ind (mind,i) env =
   Declareops.inductive_is_polymorphic (lookup_mind mind env)
 
@@ -468,10 +631,6 @@ type 'types punsafe_type_judgment = {
 
 type unsafe_type_judgment = types punsafe_type_judgment
 
-(*s Compilation of global declaration *)
-
-let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false
-
 exception Hyp_not_found
 
 let apply_to_hyp ctxt id f =
@@ -530,121 +689,3 @@ let register env field entry =
 	in
         register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
     | field -> register_one env field entry
-
-(* the Environ.register function syncrhonizes the proactive and reactive
-   retroknowledge. *)
-let dispatch =
-
-  (* subfunction used for static decompilation of int31 (after a vm_compute,
-     see pretyping/vnorm.ml for more information) *)
-  let constr_of_int31 =
-    let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
-                                    digit of i and adds 1 to it
-                                    (nth_digit_plus_one 1 3 = 2) *)
-      if Int.equal (i land (1 lsl n)) 0 then
-        1
-      else
-        2
-    in
-      fun ind -> fun digit_ind -> fun tag ->
-	let array_of_int i =
-	  Array.init 31 (fun n -> mkConstruct
-			   (digit_ind, nth_digit_plus_one i (30-n)))
-	in
-	(* We check that no bit above 31 is set to one. This assertion used to
-	fail in the VM, and led to conversion tests failing at Qed. *)
-        assert (Int.equal (tag lsr 31) 0);
-	mkApp(mkConstruct(ind, 1), array_of_int tag)
-  in
-
-  (* subfunction which dispatches the compiling information of an
-     int31 operation which has a specific vm instruction (associates
-     it to the name of the coq definition in the reactive retroknowledge) *)
-  let int31_op n op prim kn =
-    { empty_reactive_info with
-      vm_compiling = Some (Clambda.compile_prim n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
-    }
-  in
-
-fun rk value field ->
-  (* subfunction which shortens the (very common) dispatch of operations *)
-  let int31_op_from_const n op prim =
-    match kind value with
-      | Const kn ->  int31_op n op prim kn
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
-  in
-  let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
-  let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
-  match field with
-    | KInt31 (grp, Int31Type) ->
-        let int31bit =
-          (* invariant : the type of bits is registered, otherwise the function
-             would raise Not_found. The invariant is enforced in safe_typing.ml *)
-          match field with
-          | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
-          | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
-        in
-        let i31bit_type =
-          match kind int31bit with
-          | Ind (i31bit_type,_) -> i31bit_type
-          |  _ -> anomaly ~label:"Environ.register"
-              (Pp.str "Int31Bits should be an inductive type.")
-        in
-        let int31_decompilation =
-          match kind value with
-          | Ind (i31t,_) ->
-              constr_of_int31 i31t i31bit_type
-          | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "should be an inductive type.")
-        in
-        { empty_reactive_info with
-          vm_decompile_const = Some int31_decompilation;
-          vm_before_match = Some Clambda.int31_escape_before_match;
-          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
-        }
-    | KInt31 (_, Int31Constructor) ->
-        { empty_reactive_info with
-          vm_constant_static = Some Clambda.compile_structured_int31;
-          vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
-          native_constant_static = Some Nativelambda.compile_static_int31;
-          native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
-        }
-    | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
-							  CPrimitives.Int31add
-    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
-							   CPrimitives.Int31addc
-    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
-								CPrimitives.Int31addcarryc
-    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
-							   CPrimitives.Int31sub
-    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
-							    CPrimitives.Int31subc
-    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
-	                                Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
-    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
-							   CPrimitives.Int31mul
-    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
-							   CPrimitives.Int31mulc
-    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
-                                                           CPrimitives.Int31div21
-    | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
-							 CPrimitives.Int31diveucl
-    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
-                                                         CPrimitives.Int31addmuldiv
-    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
-							     CPrimitives.Int31compare
-    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
-							  CPrimitives.Int31head0
-    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
-							  CPrimitives.Int31tail0
-    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
-							 CPrimitives.Int31lor
-    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
-							  CPrimitives.Int31land
-    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
-							  CPrimitives.Int31lxor
-    | _ -> empty_reactive_info
-
-let _ = Hook.set Retroknowledge.dispatch_hook dispatch
diff --git a/kernel/environ.mli b/kernel/environ.mli
index fdd84b25b..fc45ce0e3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -28,16 +28,60 @@ open Declarations
    - a set of universe constraints
    - a flag telling if Set is, can be, or cannot be set impredicative *)
 
+type lazy_val
+
+val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit
+val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option
+val dummy_lazy_val : unit -> lazy_val
+
+(** Linking information for the native compiler *)
+type link_info =
+  | Linked of string
+  | LinkedInteractive of string
+  | NotLinked
+
+type key = int CEphemeron.key option ref
+
+type constant_key = constant_body * (link_info ref * key)
+
+type mind_key = mutual_inductive_body * link_info ref
+
+type globals = {
+  env_constants : constant_key Cmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
+  env_modules : module_body MPmap.t;
+  env_modtypes : module_type_body MPmap.t
+}
+
+type stratification = {
+  env_universes : UGraph.t;
+  env_engagement : engagement
+}
+
+type named_context_val = private {
+  env_named_ctx : Context.Named.t;
+  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+}
+
+type rel_context_val = private {
+  env_rel_ctx : Context.Rel.t;
+  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+}
+
+type env = private {
+  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_named_context : named_context_val; (* section variables *)
+  env_rel_context   : rel_context_val;
+  env_nb_rel        : int;
+  env_stratification : stratification;
+  env_typing_flags  : typing_flags;
+  retroknowledge : Retroknowledge.retroknowledge;
+  indirect_pterms : Opaqueproof.opaquetab;
+}
 
-
-
-type env
-val pre_env : env -> Pre_env.env
-val env_of_pre_env : Pre_env.env -> env
 val oracle : env -> Conv_oracle.oracle
 val set_oracle : env -> Conv_oracle.oracle -> env
 
-type named_context_val
 val eq_named_context_val : named_context_val -> named_context_val -> bool
 
 val empty_env : env
@@ -70,7 +114,9 @@ val push_rec_types   : rec_declaration -> env -> env
 (** Looks up in the context of local vars referred by indice ([rel_context]) 
    raises [Not_found] if the index points out of the context *)
 val lookup_rel    : int -> env -> Context.Rel.Declaration.t
+val lookup_rel_val : int -> env -> lazy_val
 val evaluable_rel : int -> env -> bool
+val env_of_rel     : int -> env -> env
 
 (** {6 Recurrence on [rel_context] } *)
 
@@ -102,7 +148,8 @@ val push_named_context_val  :
    raises [Not_found] if the Id.t is not found *)
 
 val lookup_named     : variable -> env -> Context.Named.Declaration.t
-val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t
+val lookup_named_val : variable -> env -> lazy_val
+val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t
 val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
@@ -112,6 +159,8 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
 
+val set_universes : env -> UGraph.t -> env
+
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
@@ -129,8 +178,9 @@ val pop_rel_context : int -> env -> env
   {6 Add entries to global environment } *)
 
 val add_constant : Constant.t -> constant_body -> env -> env
-val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info ->
+val add_constant_key : Constant.t -> constant_body -> link_info ->
   env -> env
+val lookup_constant_key :  Constant.t -> env -> constant_key
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
@@ -172,7 +222,8 @@ val lookup_projection    : Names.Projection.t -> env -> projection_body
 val is_projection : Constant.t -> env -> bool
 
 (** {5 Inductive types } *)
-val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env
+val lookup_mind_key : MutInd.t -> env -> mind_key
+val add_mind_key : MutInd.t -> mind_key -> env -> env
 val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
 
 (** Looks up in the context of global inductive names 
@@ -251,10 +302,6 @@ type 'types punsafe_type_judgment = {
 
 type unsafe_type_judgment = types punsafe_type_judgment
 
-(** {6 Compilation of global declaration } *)
-
-val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option
-
 exception Hyp_not_found
 
 (** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
@@ -264,7 +311,7 @@ val apply_to_hyp : named_context_val -> variable ->
   (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
     named_context_val
 
-val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
 
 
 
@@ -278,4 +325,4 @@ val registered : env -> field -> bool
 val register : env -> field -> Retroknowledge.entry -> env
 
 (** Native compiler *)
-val no_link_info : Pre_env.link_info
+val no_link_info : link_info
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 3fed3ed29..50713b957 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -22,17 +22,16 @@ CPrimitives
 Declareops
 Retroknowledge
 Conv_oracle
-Pre_env
+Environ
+CClosure
+Reduction
 Clambda
 Nativelambda
 Cbytegen
 Nativecode
 Nativelib
-Environ
 Csymtable
 Vm
-CClosure
-Reduction
 Vconv
 Nativeconv
 Type_errors
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1baab7c98..d63dc057b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -120,7 +120,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  const_body = def;
           const_universes = univs ;
 	  const_body_code = Option.map Cemitcodes.from_val
-                              (compile_constant_body env' cb.const_universes def) }
+                              (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
diff --git a/kernel/modops.mli b/kernel/modops.mli
index cb41a5123..ac76d28cf 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -52,7 +52,7 @@ val add_module : module_body -> env -> env
 
 (** same as add_module, but for a module whose native code has been linked by
 the native compiler. The linking information is updated. *)
-val add_linked_module : module_body -> Pre_env.link_info -> env -> env
+val add_linked_module : module_body -> link_info -> env -> env
 
 (** same, for a module type *)
 val add_module_type : ModPath.t -> module_type_body -> env -> env
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c82d982b4..0cd0ad46c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -16,7 +16,7 @@ open Util
 open Nativevalues
 open Nativeinstr
 open Nativelambda
-open Pre_env
+open Environ
 
 [@@@ocaml.warning "-32-37"]
 
@@ -1837,7 +1837,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
 
 and compile_rel env sigma univ auxdefs n =
   let open Context.Rel.Declaration in
-  let decl = Pre_env.lookup_rel n env in
+  let decl = lookup_rel n env in
   let n = List.length env.env_rel_context.env_rel_ctx - n in
   match decl with
   | LocalDef (_,t,_) ->
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 4b23cc5f8..42f2cbc2e 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -10,7 +10,7 @@
 open Names
 open Constr
 open Declarations
-open Pre_env
+open Environ
 open Nativelambda
 
 (** This file defines the mllambda code generation phase of the native
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index f51b58322..c07025660 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   aux 0 cu
 
 let native_conv_gen pb sigma env univs t1 t2 =
-  let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
-  let code, upds = mk_conv_code penv sigma prefix t1 t2 in
+  let code, upds = mk_conv_code env sigma prefix t1 t2 in
   match compile ml_filename code ~profile:false with
   | (true, fn) ->
       begin
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 12cd5fe83..a49bf62b3 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -12,7 +12,7 @@ open Names
 open Esubst
 open Constr
 open Declarations
-open Pre_env
+open Environ
 open Nativevalues
 open Nativeinstr
 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 9a1e19b3c..26bfeb7e0 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 open Names
 open Constr
-open Pre_env
+open Environ
 open Nativeinstr
 
 (** This file defines the lambda code generation phase of the native compiler *)
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index c69cf722b..8bff43632 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Declarations
-open Environ
 open Mod_subst
 open Modops
 open Nativecode
@@ -32,7 +31,7 @@ and translate_field prefix mp env acc (l,x) =
      (if !Flags.debug then
 	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
 	Feedback.msg_debug (Pp.str msg));
-     compile_constant_field (pre_env env) prefix con acc cb
+     compile_constant_field env prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
 	let id = mb.mind_packets.(0).mind_typename in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
deleted file mode 100644
index 8ebe48e20..000000000
--- a/kernel/pre_env.ml
+++ /dev/null
@@ -1,213 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Created by Benjamin Grégoire out of environ.ml for better
-   modularity in the design of the bytecode virtual evaluation
-   machine, Dec 2005 *)
-(* Bug fix by Jean-Marc Notin *)
-
-(* This file defines the type of kernel environments *)
-
-open Util
-open Names
-open Declarations
-
-module NamedDecl = Context.Named.Declaration
-
-(* The type of environments. *)
-
-(* The key attached to each constant is used by the VM to retrieve previous *)
-(* evaluations of the constant. It is essentially an index in the symbols table *)
-(* used by the VM. *)
-type key = int CEphemeron.key option ref 
-
-(** Linking information for the native compiler. *)
-
-type link_info =
-  | Linked of string
-  | LinkedInteractive of string
-  | NotLinked
-
-type constant_key = constant_body * (link_info ref * key)
-
-type mind_key = mutual_inductive_body * link_info ref
-
-type globals = {
-  env_constants : constant_key Cmap_env.t;
-  env_inductives : mind_key Mindmap_env.t;
-  env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t}
-
-type stratification = {
-  env_universes : UGraph.t;
-  env_engagement : engagement
-}
-
-type val_kind =
-    | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key
-    | VKnone
-
-type lazy_val = val_kind ref
-
-let force_lazy_val vk = match !vk with
-| VKnone -> None
-| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None
-
-let dummy_lazy_val () = ref VKnone
-let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
-
-type named_context_val = {
-  env_named_ctx : Context.Named.t;
-  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
-}
-
-type rel_context_val = {
-  env_rel_ctx : Context.Rel.t;
-  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
-}
-
-type env = {
-  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
-  env_named_context : named_context_val; (* section variables *)
-  env_rel_context   : rel_context_val;
-  env_nb_rel        : int;
-  env_stratification : stratification;
-  env_typing_flags  : typing_flags;
-  retroknowledge : Retroknowledge.retroknowledge;
-  indirect_pterms : Opaqueproof.opaquetab;
-}
-
-let empty_named_context_val = {
-  env_named_ctx = [];
-  env_named_map = Id.Map.empty;
-}
-
-let empty_rel_context_val = {
-  env_rel_ctx = [];
-  env_rel_map = Range.empty;
-}
-
-let empty_env = {
-  env_globals = {
-    env_constants = Cmap_env.empty;
-    env_inductives = Mindmap_env.empty;
-    env_modules = MPmap.empty;
-    env_modtypes = MPmap.empty};
-  env_named_context = empty_named_context_val;
-  env_rel_context = empty_rel_context_val;
-  env_nb_rel = 0;
-  env_stratification = {
-    env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet };
-  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
-  retroknowledge = Retroknowledge.initial_retroknowledge;
-  indirect_pterms = Opaqueproof.empty_opaquetab }
-
-
-(* Rel context *)
-
-let nb_rel env = env.env_nb_rel
-
-let push_rel_context_val d ctx = {
-  env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx;
-  env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map;
-}
-
-let match_rel_context_val ctx = match ctx.env_rel_ctx with
-| [] -> None
-| decl :: rem ->
-  let (_, lval) = Range.hd ctx.env_rel_map in
-  let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in
-  Some (decl, lval, ctx)
-
-let push_rel d env =
-    { env with
-      env_rel_context = push_rel_context_val d env.env_rel_context;
-      env_nb_rel = env.env_nb_rel + 1 }
-
-let lookup_rel n env =
-  try fst (Range.get env.env_rel_context.env_rel_map (n - 1))
-  with Invalid_argument _ -> raise Not_found
-
-let lookup_rel_val n env =
-  try snd (Range.get env.env_rel_context.env_rel_map (n - 1))
-  with Invalid_argument _ -> raise Not_found
-
-let rel_skipn n ctx = {
-  env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx;
-  env_rel_map = Range.skipn n ctx.env_rel_map;
-}
-
-let env_of_rel n env =
-  { env with
-    env_rel_context = rel_skipn n env.env_rel_context;
-    env_nb_rel = env.env_nb_rel - n
-  }
-
-(* Named context *)
-
-let push_named_context_val_val d rval ctxt =
-(*   assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
-  {
-    env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
-    env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
-  }
-
-let push_named_context_val d ctxt =
-  push_named_context_val_val d (ref VKnone) ctxt
-
-let match_named_context_val c = match c.env_named_ctx with
-| [] -> None
-| decl :: ctx ->
-  let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
-  let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
-  let cval = { env_named_ctx = ctx; env_named_map = map } in
-  Some (decl, v, cval)
-
-let map_named_val f ctxt =
-  let open Context.Named.Declaration in
-  let fold accu d =
-    let d' = map_constr f d in
-    let accu =
-      if d == d' then accu
-      else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu
-    in
-    (accu, d')
-  in
-  let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  if map == ctxt.env_named_map then ctxt
-  else { env_named_ctx = ctx; env_named_map = map }
-
-let push_named d env =
-  {env with env_named_context = push_named_context_val d env.env_named_context}
-
-let lookup_named id env =
-  fst (Id.Map.find id env.env_named_context.env_named_map)
-
-let lookup_named_val id env =
-  snd(Id.Map.find id env.env_named_context.env_named_map)
-
-(* Warning all the names should be different *)
-let env_of_named id env = env
-
-(* Global constants *)
-
-let lookup_constant_key kn env =
-  Cmap_env.find kn env.env_globals.env_constants
-
-let lookup_constant kn env =
-  fst (Cmap_env.find kn env.env_globals.env_constants)
-
-(* Mutual Inductives *)
-let lookup_mind kn env =
-  fst (Mindmap_env.find kn env.env_globals.env_inductives)
-
-let lookup_mind_key kn env =
-  Mindmap_env.find kn env.env_globals.env_inductives
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
deleted file mode 100644
index b05074814..000000000
--- a/kernel/pre_env.mli
+++ /dev/null
@@ -1,108 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Constr
-open Declarations
-
-(** The type of environments. *)
-
-type link_info =
-  | Linked of string
-  | LinkedInteractive of string
-  | NotLinked
-
-type key = int CEphemeron.key option ref 
-
-type constant_key = constant_body * (link_info ref * key)
-
-type mind_key = mutual_inductive_body * link_info ref
-
-type globals = {
-  env_constants : constant_key Cmap_env.t;
-  env_inductives : mind_key Mindmap_env.t;
-  env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t}
-
-type stratification = {
-  env_universes : UGraph.t;
-  env_engagement : engagement
-}
-
-type lazy_val
-
-val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option
-val dummy_lazy_val : unit -> lazy_val
-val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit
-
-type named_context_val = private {
-  env_named_ctx : Context.Named.t;
-  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
-}
-
-type rel_context_val = private {
-  env_rel_ctx : Context.Rel.t;
-  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
-}
-
-type env = {
-    env_globals       : globals;
-    env_named_context : named_context_val;
-    env_rel_context   : rel_context_val;
-    env_nb_rel        : int;
-    env_stratification : stratification;
-    env_typing_flags  : typing_flags;
-    retroknowledge : Retroknowledge.retroknowledge;
-    indirect_pterms : Opaqueproof.opaquetab;
-}
-
-val empty_named_context_val : named_context_val
-
-val empty_env : env
-
-(** Rel context *)
-
-val empty_rel_context_val : rel_context_val
-val push_rel_context_val :
-  Context.Rel.Declaration.t -> rel_context_val -> rel_context_val
-val match_rel_context_val  :
-  rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option
-
-val nb_rel         : env -> int
-val push_rel       : Context.Rel.Declaration.t -> env -> env
-val lookup_rel     : int -> env -> Context.Rel.Declaration.t
-val lookup_rel_val : int -> env -> lazy_val
-val env_of_rel     : int -> env -> env
-
-(** Named context *)
-
-val push_named_context_val  :
-    Context.Named.Declaration.t -> named_context_val -> named_context_val
-val push_named_context_val_val  :
-    Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
-val match_named_context_val  :
-  named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
-val map_named_val :
-   (constr -> constr) -> named_context_val -> named_context_val
-
-val push_named       : Context.Named.Declaration.t -> env -> env
-val lookup_named     : Id.t -> env -> Context.Named.Declaration.t
-val lookup_named_val : Id.t -> env -> lazy_val
-val env_of_named     : Id.t -> env -> env
-
-(** Global constants *)
-
-
-val lookup_constant_key : Constant.t -> env -> constant_key
-val lookup_constant : Constant.t -> env -> constant_body
-
-(** Mutual Inductives *)
-val lookup_mind_key : MutInd.t -> env -> mind_key
-val lookup_mind : MutInd.t -> env -> mutual_inductive_body
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0334e7a9e..281c37b85 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -134,7 +134,7 @@ val get_native_before_match_info : retroknowledge -> entry ->
 				   Nativeinstr.lambda -> Nativeinstr.lambda
 
 
-(** the following functions are solely used in Pre_env and Environ to implement
+(** the following functions are solely used in Environ and Safe_typing to implement
    the functions  register and unregister (and mem) of Environ *)
 val add_field : retroknowledge -> field -> entry -> retroknowledge
 val mem : retroknowledge -> field -> bool
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index de2a890fb..e07833204 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -59,6 +59,7 @@
    etc.
 *)
 
+open CErrors
 open Util
 open Names
 open Declarations
@@ -914,16 +915,12 @@ let register field value by_clause senv =
 but it is meant to become a replacement for environ.register *)
 let register_inline kn senv =
   let open Environ in
-  let open Pre_env in
   if not (evaluable_constant kn senv.env) then
     CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected");
-  let env = pre_env senv.env in
+  let env = senv.env in
   let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in
-  let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in
-  let new_globals = { env.env_globals with env_constants = new_constants } in
-  let env = { env with env_globals = new_globals } in
-  { senv with env = env_of_pre_env env }
+  let env = add_constant kn cb env in { senv with env}
 
 let add_constraints c =
   add_constraints
@@ -953,3 +950,125 @@ Would this be correct with respect to undo's and stuff ?
 let set_strategy e k l = { e with env =
    (Environ.set_oracle e.env
       (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
+
+(** Register retroknowledge hooks *)
+
+open Retroknowledge
+
+(* the Environ.register function syncrhonizes the proactive and reactive
+   retroknowledge. *)
+let dispatch =
+
+  (* subfunction used for static decompilation of int31 (after a vm_compute,
+     see pretyping/vnorm.ml for more information) *)
+  let constr_of_int31 =
+    let nth_digit_plus_one i n = (* calculates the nth (starting with 0)
+                                    digit of i and adds 1 to it
+                                    (nth_digit_plus_one 1 3 = 2) *)
+      if Int.equal (i land (1 lsl n)) 0 then
+        1
+      else
+        2
+    in
+      fun ind -> fun digit_ind -> fun tag ->
+        let array_of_int i =
+          Array.init 31 (fun n -> Constr.mkConstruct
+                           (digit_ind, nth_digit_plus_one i (30-n)))
+        in
+        (* We check that no bit above 31 is set to one. This assertion used to
+        fail in the VM, and led to conversion tests failing at Qed. *)
+        assert (Int.equal (tag lsr 31) 0);
+        Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag)
+  in
+
+  (* subfunction which dispatches the compiling information of an
+     int31 operation which has a specific vm instruction (associates
+     it to the name of the coq definition in the reactive retroknowledge) *)
+  let int31_op n op prim kn =
+    { empty_reactive_info with
+      vm_compiling = Some (Clambda.compile_prim n op kn);
+      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
+    }
+  in
+
+fun rk value field ->
+  (* subfunction which shortens the (very common) dispatch of operations *)
+  let int31_op_from_const n op prim =
+    match Constr.kind value with
+      | Constr.Const kn ->  int31_op n op prim kn
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
+  in
+  let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
+  let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
+  match field with
+    | KInt31 (grp, Int31Type) ->
+        let int31bit =
+          (* invariant : the type of bits is registered, otherwise the function
+             would raise Not_found. The invariant is enforced in safe_typing.ml *)
+          match field with
+          | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
+        in
+        let i31bit_type =
+          match Constr.kind int31bit with
+          | Constr.Ind (i31bit_type,_) -> i31bit_type
+          |  _ -> anomaly ~label:"Environ.register"
+              (Pp.str "Int31Bits should be an inductive type.")
+        in
+        let int31_decompilation =
+          match Constr.kind value with
+          | Constr.Ind (i31t,_) ->
+              constr_of_int31 i31t i31bit_type
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "should be an inductive type.")
+        in
+        { empty_reactive_info with
+          vm_decompile_const = Some int31_decompilation;
+          vm_before_match = Some Clambda.int31_escape_before_match;
+          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
+        }
+    | KInt31 (_, Int31Constructor) ->
+        { empty_reactive_info with
+          vm_constant_static = Some Clambda.compile_structured_int31;
+          vm_constant_dynamic = Some Clambda.dynamic_int31_compilation;
+          native_constant_static = Some Nativelambda.compile_static_int31;
+          native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
+        }
+    | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
+                                                          CPrimitives.Int31add
+    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
+                                                           CPrimitives.Int31addc
+    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
+                                                                CPrimitives.Int31addcarryc
+    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
+                                                           CPrimitives.Int31sub
+    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
+                                                            CPrimitives.Int31subc
+    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
+                                        Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
+    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
+                                                           CPrimitives.Int31mul
+    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
+                                                           CPrimitives.Int31mulc
+    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
+                                                           CPrimitives.Int31div21
+    | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
+                                                         CPrimitives.Int31diveucl
+    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
+                                                         CPrimitives.Int31addmuldiv
+    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
+                                                             CPrimitives.Int31compare
+    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
+                                                          CPrimitives.Int31head0
+    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
+                                                          CPrimitives.Int31tail0
+    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
+                                                         CPrimitives.Int31lor
+    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
+                                                          CPrimitives.Int31land
+    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
+                                                          CPrimitives.Int31lxor
+    | _ -> empty_reactive_info
+
+let _ = Hook.set Retroknowledge.dispatch_hook dispatch
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e621a61c7..7352c1882 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -460,7 +460,7 @@ let build_constant_declaration kn env result =
   let tps = 
     let res =
       match result.cook_proj with
-      | None -> compile_constant_body env univs def
+      | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def
       | Some pb ->
 	(* The compilation of primitive projections is a bit tricky, because
            they refer to themselves (the body of p looks like fun c =>
@@ -480,7 +480,7 @@ let build_constant_declaration kn env result =
 	    }
 	in
 	let env = add_constant kn cb env in
-	compile_constant_body env univs def
+        Cbytegen.compile_constant_body ~fail_on_error:false env univs def
     in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 6f350951c..4e4168922 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -6,9 +6,6 @@ open Vm
 open Vmvalues
 open Csymtable
 
-let val_of_constr env c =
-  val_of_constr (pre_env env) c
-
 (* Test la structure des piles *)
 
 let compare_zipper z1 z2 =
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 620f6b5e8..1a3184898 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Constr
-open Environ
 open Reduction
 
 (**********************************************************************
@@ -19,6 +18,3 @@ val vm_conv : conv_pb -> types kernel_conversion_function
 (** A conversion function parametrized by a universe comparator. Used outside of
     the kernel. *)
 val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
-
-(** Precompute a VM value from a constr *)
-val val_of_constr : env -> constr -> Vmvalues.values
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index fb6be430f..5463893ad 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -52,7 +52,7 @@ let instantiate_tac n c ido =
     match ido with
 	ConclLocation () -> evar_list sigma (pf_concl gl)
       | HypLocation (id,hloc) ->
-	  let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
+          let decl = Environ.lookup_named id (pf_env gl) in
 	    match hloc with
 		InHyp ->
 		  (match decl with
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 85911394f..978ceed1e 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -457,13 +457,12 @@ let native_norm env sigma c ty =
   if not Coq_config.native_compiler then
     user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
   else
-  let penv = Environ.pre_env env in
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
   *)
   let ml_filename, prefix = Nativelib.get_ml_filename () in
-  let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in
+  let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
   let profile = get_profiling_enabled () in
   match Nativelib.compile ml_filename code ~profile:profile with
     | true, fn ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 6bd75c93d..68f9610d1 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -215,10 +215,7 @@ let judge_of_cast env sigma cj k tj =
              uj_type = expected_type }
 
 let enrich_env env sigma =
-  let penv = Environ.pre_env env in
-  let penv' = Pre_env.({ penv with env_stratification =
-    { penv.env_stratification with env_universes = Evd.universes sigma } }) in
-  Environ.env_of_pre_env penv'
+  set_universes env @@ Evd.universes sigma
 
 let check_fix env sigma pfix =
   let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 049c3aff5..a1ba4a6a9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -383,7 +383,7 @@ let cbv_vm env sigma c t  =
   (** This evar-normalizes terms beforehand *)
   let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
-  let v = Vconv.val_of_constr env c in
+  let v = Csymtable.val_of_constr env c in
   EConstr.of_constr (nf_val env sigma v t)
 
 let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1ce4e194..a2b8446bb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -266,7 +266,7 @@ let print_namespace ns =
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
   | _ -> false in
-  let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
+  let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in
   let constants_in_namespace =
     Cmap_env.fold (fun c (body,_) acc ->
       let kn = Constant.user c in