27 files changed, 254 insertions, 195 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
new file mode 100644
index 0000000000..3a714a8a59
--- /dev/null
+++ b/kernel/byterun/dune
@@ -0,0 +1,10 @@
+(library
+ (name byterun)
+ (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
+ (public_name coq.vm)
+ (c_names coq_fix_code coq_memory coq_values coq_interp))
+
+(rule
+ (targets coq_jumptbl.h)
+ (deps (:h-file coq_instruct.h))
+ (action (run ./make_jumptbl.sh %{h-file} %{targets})))
diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh
new file mode 100755
index 0000000000..eacd4daac8
--- /dev/null
+++ b/kernel/byterun/make_jumptbl.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2}
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index ac4c6c52c6..fd9394025a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -31,7 +31,6 @@ open Environ
 open Esubst
 
 let stats = ref false
-let share = ref true
 
 (* Profiling *)
 let beta = ref 0
@@ -266,6 +265,7 @@ type 'a infos_cache = {
   i_env : env;
   i_sigma : existential -> constr option;
   i_rels : (Constr.rel_declaration * lazy_val) Range.t;
+  i_share : bool;
 }
 
 and 'a infos = {
@@ -313,12 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref =
 let evar_value cache ev =
   cache.i_sigma ev
 
-let create mk_cl flgs env evars =
+let create ~repr ~share flgs env evars =
   let cache =
-    { i_repr = mk_cl;
+    { i_repr = repr;
       i_env = env;
       i_sigma = evars;
       i_rels = env.env_rel_context.env_rel_map;
+      i_share = share;
     }
   in { i_flags = flgs; i_cache = cache }
 
@@ -384,8 +385,8 @@ let mk_red f = {norm=Red;term=f}
 
 (* Could issue a warning if no is still Red, pointing out that we loose
    sharing. *)
-let update v1 no t =
-  if !share then
+let update ~share v1 no t =
+  if share then
     (v1.norm <- no;
      v1.term <- t;
      v1)
@@ -498,14 +499,16 @@ let compact_stack head stk =
         (* Be sure to create a new cell otherwise sharing would be
            lost by the update operation *)
         let h' = lft_fconstr depth head in
-        let _ = update m h'.norm h'.term in
+        (** The stack contains [Zupdate] marks only if in sharing mode *)
+        let _ = update ~share:true m h'.norm h'.term in
         strip_rec depth s
     | stk -> zshift depth stk in
   strip_rec 0 stk
 
 (* Put an update mark in the stack, only if needed *)
-let zupdate m s =
-  if !share && begin match m.norm with Red -> true | _ -> false end
+let zupdate info m s =
+  let share = info.i_cache.i_share in
+  if share && begin match m.norm with Red -> true | _ -> false end
   then
     let s' = compact_stack m s in
     let _ = m.term <- FLOCKED in
@@ -698,7 +701,8 @@ let rec zip m stk =
     | Zshift(n)::s ->
         zip (lift_fconstr n m) s
     | Zupdate(rf)::s ->
-        zip (update rf m.norm m.term) s
+      (** The stack contains [Zupdate] marks only if in sharing mode *)
+        zip (update ~share:true rf m.norm m.term) s
 
 let fapp_stack (m,stk) = zip m stk
 
@@ -718,7 +722,8 @@ let strip_update_shift_app_red head stk =
         strip_rec (Zapp args :: rstk)
           {norm=h.norm;term=FApp(h,args)} depth s
     | Zupdate(m)::s ->
-        strip_rec rstk (update m h.norm h.term) depth s
+      (** The stack contains [Zupdate] marks only if in sharing mode *)
+        strip_rec rstk (update ~share:true m h.norm h.term) depth s
     | stk -> (depth,List.rev rstk, stk) in
   strip_rec [] head 0 stk
 
@@ -743,7 +748,8 @@ let get_nth_arg head n stk =
             List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
-        strip_rec rstk (update m h.norm h.term) n s
+        (** The stack contains [Zupdate] mark only if in sharing mode *)
+        strip_rec rstk (update ~share:true m h.norm h.term) n s
     | s -> (None, List.rev rstk @ s) in
   strip_rec [] head n stk
 
@@ -752,7 +758,8 @@ let get_nth_arg head n stk =
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
-        let _hd = update r Cstr (FLambda(n,tys,f,e)) in
+        (** The stack contains [Zupdate] mark only if in sharing mode *)
+        let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in
         get_args n tys f e s
     | Zshift k :: s ->
         get_args n tys f (subs_shft (k,e)) s
@@ -889,10 +896,10 @@ let unfold_projection info p =
 let rec knh info m stk =
   match m.term with
     | FLIFT(k,a) -> knh info a (zshift k stk)
-    | FCLOS(t,e) -> knht info e t (zupdate m stk)
+    | FCLOS(t,e) -> knht info e t (zupdate info m stk)
     | FLOCKED -> assert false
-    | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
-    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk)
+    | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
+    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -901,7 +908,7 @@ let rec knh info m stk =
     | FProj (p,c) ->
       (match unfold_projection info p with
        | None -> (m, stk)
-       | Some s -> knh info c (s :: zupdate m stk))
+       | Some s -> knh info c (s :: zupdate info m stk))
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
@@ -1019,10 +1026,11 @@ let rec zip_term zfun m stk =
    2- tries to rebuild the term. If a closure still has to be computed,
       calls itself recursively. *)
 let rec kl info tab m =
+  let share = info.i_cache.i_share in
   if is_val m then (incr prune; term_of_fconstr m)
   else
     let (nm,s) = kni info tab m [] in
-    let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
+    let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
     zip_term (kl info tab) (norm_head info tab nm) s
 
 (* no redex: go up for atoms and already normalized terms, go down
@@ -1078,14 +1086,15 @@ let whd_stack infos tab m stk = match m.norm with
   knh infos m stk
 | Red | Cstr ->
   let k = kni infos tab m stk in
-  let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
+  let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
   k
 
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
-  create (fun _ _ c -> inject c) flgs env evars
+  let share = (Environ.typing_flags env).Declarations.share_reduction in
+  create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
 
 let create_tab () = KeyTable.create 17
 
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1e3e7b48ac..6121b3a1ec 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -15,7 +15,6 @@ open Esubst
 
 (** Flags for profiling reductions. *)
 val stats : bool ref
-val share : bool ref
 
 val with_stats: 'a Lazy.t -> 'a
 
@@ -106,8 +105,13 @@ type 'a infos = {
   i_cache : 'a infos_cache }
 
 val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
-val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
-  (existential -> constr option) -> 'a infos
+val create:
+  repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
+  share:bool ->
+  reds ->
+  env ->
+  (existential -> constr option) ->
+  'a infos
 val create_tab : unit -> 'a infos_tab
 val evar_value : 'a infos_cache -> existential -> constr option
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index c06358054e..657478a106 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -24,6 +24,7 @@ open Declarations
 open Univ
 
 module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
 
 (*s Cooking the constants. *)
 
@@ -140,11 +141,31 @@ let expmod_constr cache modlist c =
   if is_empty_modlist modlist then c
   else substrec c
 
-let abstract_constant_type =
-   List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
+(** Transforms a named context into a rel context. Also returns the list of
+    variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to
+    abstract a term that lived in that context. *)
+let abstract_context hyps =
+  let fold decl (ctx, subst) =
+    let id, decl = match decl with
+    | NamedDecl.LocalDef (id, b, t) ->
+      let b = Vars.subst_vars subst b in
+      let t = Vars.subst_vars subst t in
+      id, RelDecl.LocalDef (Name id, b, t)
+    | NamedDecl.LocalAssum (id, t) ->
+      let t = Vars.subst_vars subst t in
+      id, RelDecl.LocalAssum (Name id, t)
+    in
+    (decl :: ctx, id :: subst)
+  in
+  Context.Named.fold_outside fold hyps ~init:([], [])
+
+let abstract_constant_type t (hyps, subst) =
+  let t = Vars.subst_vars subst t in
+  List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps
 
-let abstract_constant_body =
-  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
+let abstract_constant_body c (hyps, subst) =
+  let c = Vars.subst_vars subst c in
+  it_mkLambda_or_LetIn c hyps
 
 type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
@@ -173,6 +194,7 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
   let cache = RefTable.create 13 in
   let expmod = expmod_constr_subst cache modlist subst in
   let hyps = Context.Named.map expmod vars in
+  let hyps = abstract_context hyps in
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst auctx0 =
@@ -207,12 +229,13 @@ let cook_constant ~hcons { from = cb; info } =
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst abs_ctx in
   let expmod = expmod_constr_subst cache modlist usubst in
-  let hyps = Context.Named.map expmod abstract in
+  let hyps0 = Context.Named.map expmod abstract in
+  let hyps = abstract_context hyps0 in
   let map c =
     let c = abstract_constant_body (expmod c) hyps in
     if hcons then Constr.hcons c else c
   in
-  let body = on_body modlist (hyps, usubst, abs_ctx)
+  let body = on_body modlist (hyps0, usubst, abs_ctx)
     map
     cb.const_body
   in
@@ -220,7 +243,7 @@ let cook_constant ~hcons { from = cb; info } =
     Context.Named.fold_outside (fun decl hyps ->
       List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
-      hyps ~init:cb.const_hyps in
+      hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
   {
     cook_body = body;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0811eb72fd..1d49550442 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -65,6 +65,7 @@ type typing_flags = {
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
+  share_reduction : bool; (** Use by-need reduction algorithm *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index bbe4bc0dcb..51ec3defb3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -21,6 +21,7 @@ let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
   conv_oracle = oracle;
+  share_reduction = true;
 }
 
 (** {6 Arities } *)
@@ -305,13 +306,6 @@ let hcons_mind mib =
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
-(** {6 Stm machinery } *)
-
-let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
-  | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
-
 (** Hashconsing of modules *)
 
 let hcons_functorize hty he hself f = match f with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index f91e69807f..35490ceef9 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -11,7 +11,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Entries
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-(** Side effects *)
-
-val string_of_side_effect : side_effect -> string
-
 (** {6 Inductive types} *)
 
 val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/dune b/kernel/dune
new file mode 100644
index 0000000000..011af9c28c
--- /dev/null
+++ b/kernel/dune
@@ -0,0 +1,15 @@
+(library
+ (name kernel)
+ (synopsis "The Coq Kernel")
+ (public_name coq.kernel)
+ (wrapped false)
+ (modules_without_implementation cinstr nativeinstr)
+ (libraries clib config lib byterun))
+
+(rule
+ (targets copcodes.ml)
+ (deps (:h-file byterun/coq_instruct.h) make-opcodes)
+ (action (run ./make_opcodes.sh %{h-file} %{targets})))
+
+(documentation
+ (package coq))
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 40873bea76..94248ad26b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,11 +120,14 @@ type seff_env =
      Same as the constant_body's but not in an ephemeron *)
   | `Opaque of Constr.t * Univ.ContextSet.t ]
 
-type side_eff =
-  | SEsubproof of Constant.t * Declarations.constant_body * seff_env
-  | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string
-
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff;
+(** Not used by the kernel. *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type side_eff = {
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : side_effect_role;
 }
diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh
new file mode 100755
index 0000000000..bb8aba2f07
--- /dev/null
+++ b/kernel/make_opcodes.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+script_dir="$(dirname "$0")"
+tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' | awk -f "$script_dir"/make-opcodes > "${2}"
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index cc35a70cbf..ad10c86945 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1067,12 +1067,11 @@ let ml_of_instance instance u =
      let tyn = fresh_lname Anonymous in
      let i = push_symbol (SymbMeta mv) in
      MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
-  | Levar(evk,ty,args) ->
-     let tyn = fresh_lname Anonymous in
+  | Levar(evk, args) ->
      let i = push_symbol (SymbEvar evk) in
+     (** Arguments are *not* reversed in evar instances in native compilation *)
      let args = MLarray(Array.map (ml_of_lam env l) args) in
-     MLlet(tyn, ml_of_lam env l ty,
-       MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|]))
+     MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|])
   | Lprod(dom,codom) ->
       let dom = ml_of_lam env l dom in
       let codom = ml_of_lam env l codom in
@@ -1749,7 +1748,7 @@ let pp_mllam fmt l =
     | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start
     | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
     | Mk_var id ->
-        Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id)
+        Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id)
     | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
     | Is_int -> Format.fprintf fmt "is_int"
     | Cast_accu -> Format.fprintf fmt "cast_accu"
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 931b8bbc86..c75dde843e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu =
     match a1, a2 with
     | Ameta (m1,_), Ameta (m2,_) ->
       if Int.equal m1 m2 then cu else raise NotConvertible
-    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+    | Aevar (ev1, args1), Aevar (ev2, args2) ->
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 5075bd3d14..2d8e2ba2f0 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -25,7 +25,7 @@ and lambda =
   | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
-  | Levar         of Evar.t * lambda (* type *) * lambda array (* arguments *)
+  | Levar         of Evar.t * lambda array (* arguments *)
   | Lprod         of lambda * lambda 
   | Llam          of Name.t array * lambda  
   | Llet          of Name.t * lambda * lambda
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cec0ee57d5..122fe95df4 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -23,7 +23,6 @@ exception NotClosed
 
 type evars =
     { evars_val : existential -> constr option;
-      evars_typ : existential -> types;
       evars_metas : metavariable -> types }
 
 (*s Constructors *)
@@ -88,7 +87,7 @@ let get_const_prefix env c =
 let rec map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _
-  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
+  | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -139,6 +138,9 @@ let rec map_lam_with_binders g f n lam =
   | Luint u ->
     let u' = map_uint g f n u in
     if u == u' then lam else Luint u'
+  | Levar (evk, args) ->
+    let args' = Array.Smart.map (f n) args in
+    if args == args' then lam else Levar (evk, args')
 
 and map_uint g f n u =
   match u with
@@ -386,13 +388,10 @@ let is_lazy env prefix t =
 
 let evar_value sigma ev = sigma.evars_val ev
 
-let evar_type sigma ev = sigma.evars_typ ev
-
 let meta_type sigma mv = sigma.evars_metas mv
 
 let empty_evars =
   { evars_val = (fun _ -> None);
-    evars_typ = (fun _ -> assert false);
     evars_metas = (fun _ -> assert false) }
 
 let empty_ids = [||]
@@ -420,9 +419,8 @@ let rec lambda_of_constr cache env sigma c =
   | Evar (evk,args as ev) ->
      (match evar_value sigma ev with
      | None ->
-	let ty = evar_type sigma ev in
         let args = Array.map (lambda_of_constr cache env sigma) args in
-        Levar(evk, lambda_of_constr cache env sigma ty, args)
+        Levar(evk, args)
      | Some t -> lambda_of_constr cache env sigma t)
 
   | Cast (c, _, _) -> lambda_of_constr cache env sigma c
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index efe1700cd7..7b20258929 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -15,7 +15,6 @@ open Nativeinstr
 (** This file defines the lambda code generation phase of the native compiler *)
 type evars =
     { evars_val : existential -> constr option;
-      evars_typ : existential -> types;
       evars_metas : metavariable -> types }
 
 val empty_evars : evars
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 91f6add1c3..3bf23f1468 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -63,7 +63,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t * t array
+  | Aevar of Evar.t * t array
   | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
@@ -135,8 +135,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty args =
-  mk_accu (Aevar (ev,ty,args))
+let mk_evar_accu ev args =
+  mk_accu (Aevar (ev, args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 6bbf15160c..10689941e8 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -53,7 +53,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t (* type *) * t array (* arguments *)
+  | Aevar of Evar.t * t array (* arguments *)
   | Aproj of (inductive * int) * accumulator
 
 (* Constructors *)
@@ -70,7 +70,7 @@ val mk_prod_accu : Name.t -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
 val mk_cofix_accu : int -> t array -> t array -> t
 val mk_meta_accu : metavariable -> t
-val mk_evar_accu : Evar.t -> t -> t array -> t
+val mk_evar_accu : Evar.t -> t array -> t
 val mk_proj_accu : (inductive * int) -> accumulator -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f87ec9e023..6c87ff570f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -210,13 +210,8 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-type private_constant = Entries.side_effect
 type private_constants = Term_typing.side_effects
 
-type private_constant_role = Term_typing.side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-
 let empty_private_constants = Term_typing.empty_seff
 let add_private = Term_typing.add_seff
 let concat_private = Term_typing.concat_seff
@@ -225,44 +220,38 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants = Term_typing.uniq_seff
 
+let make_eff env cst r =
+  let open Entries in
+  let cbo = Environ.lookup_constant cst env.env in
+  {
+    seff_constant = cst;
+    seff_body = cbo;
+    seff_env = get_opaque_body env.env cbo;
+    seff_role = r;
+  }
+
 let private_con_of_con env c =
-  let cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+  let open Entries in
+  let eff = [make_eff env c Subproof] in
+  add_private env.revstruct eff empty_private_constants
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = CEphemeron.create env.revstruct;
-    Entries.eff      = Entries.SEscheme(
-      List.map (fun (i,c) ->
-        let cbo = Environ.lookup_constant c env.env in
-        i, c, cbo, get_opaque_body env.env cbo) cl,
-      kind) }
+  let open Entries in
+  let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
+  add_private env.revstruct eff empty_private_constants
 
 let universes_of_private eff =
-  let open Declarations in
-  List.fold_left
-    (fun acc { Entries.eff } ->
-       match eff with
-       | Entries.SEscheme (l,s) ->
-         List.fold_left
-           (fun acc (_,_,cb,c) ->
-              let acc = match c with
-                | `Nothing -> acc
-                | `Opaque (_, ctx) -> ctx :: acc
-              in
-              match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-           )
-           acc l
-       | Entries.SEsubproof (c, cb, e) ->
-         match cb.const_universes with
-              | Monomorphic_const ctx ->
-                ctx :: acc
-              | Polymorphic_const _ -> acc
-    )
-    [] (Term_typing.uniq_seff eff)
+  let open Entries in
+  let fold acc eff =
+    let acc = match eff.seff_env with
+    | `Nothing -> acc
+    | `Opaque (_, ctx) -> ctx :: acc
+    in
+    match eff.seff_body.const_universes with
+    | Monomorphic_const ctx -> ctx :: acc
+    | Polymorphic_const _ -> acc
+  in
+  List.fold_left fold [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -489,7 +478,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  Constant.t * private_constant_role
+  Constant.t * Entries.side_effect_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index aca77ccd13..502e2970a1 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 (** {6 Stm machinery } *)
 
-type private_constant
 type private_constants
 
-type private_constant_role =
-  | Subproof
-  | Schema of inductive * string
-
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effect list
+  private_constants -> Entries.side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
 val empty_private_constants : private_constants
-val add_private : private_constant -> private_constants -> private_constants
-(** Add a constant to a list of private constants. The former must be more
-    recent than all constants appearing in the latter, i.e. one should not
-    create a dependency cycle. *)
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_con_of_con : safe_environment -> Constant.t -> private_constant
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant
+val private_con_of_con : safe_environment -> Constant.t -> private_constants
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
 
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
@@ -105,7 +96,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  Constant.t * private_constant_role
+  Constant.t * Entries.side_effect_role
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.definition_entry ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1f7ee145a2..43351737e5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,16 +27,10 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
-let equal_eff e1 e2 =
-  let open Entries in
-  match e1, e2 with
-  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
-        Names.Constant.equal c1 c2
-  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
-        CList.for_all2eq
-          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
-          cl1 cl2
-  | _ -> false
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
+  eff      : side_eff list;
+}
 
 module SideEffects :
 sig
@@ -48,17 +42,11 @@ sig
 end =
 struct
 
-let compare_seff e1 e2 = match e1, e2 with
-| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
-| SEscheme (cl1, _), SEscheme (cl2, _) ->
-  let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
-  CList.compare cmp cl1 cl2
-| SEsubproof _, SEscheme _ -> -1
-| SEscheme _, SEsubproof _ -> 1
-
 module SeffOrd = struct
 type t = side_effect
-let compare e1 e2 = compare_seff e1.eff e2.eff
+let compare e1 e2 =
+  let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
+  List.compare cmp e1.eff e2.eff
 end
 
 module SeffSet = Set.Make(SeffOrd)
@@ -83,10 +71,14 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 let uniq_seff_rev = SideEffects.repr
-let uniq_seff l = List.rev (SideEffects.repr l)
+let uniq_seff l =
+  let ans = List.rev (SideEffects.repr l) in
+  List.map_append (fun { eff } -> eff) ans
 
 let empty_seff = SideEffects.empty
-let add_seff = SideEffects.add
+let add_seff mb eff effs =
+  let from_env = CEphemeron.create mb in
+  SideEffects.add { eff; from_env } effs
 let concat_seff = SideEffects.concat
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
@@ -94,11 +86,8 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 let inline_side_effects env body ctx side_eff =
   (** First step: remove the constants that are still in the environment *)
   let filter { eff = se; from_env = mb } =
-    let cbl = match se with
-    | SEsubproof (c, cb, b) -> [c, cb, b]
-    | SEscheme (cl,_) ->
-      List.map (fun (_, c, cb, b) -> c, cb, b) cl
-    in
+    let map e = (e.seff_constant, e.seff_body, e.seff_env) in
+    let cbl = List.map map se in
     let not_exists (c,_,_) =
       try ignore(Environ.lookup_constant c env); false
       with Not_found -> true in 
@@ -468,58 +457,50 @@ let constant_entry_of_side_effect cb u =
     const_entry_inline_code = cb.const_inline_code }
 ;;
 
-let turn_direct (kn,cb,u,r as orig) =
-  match cb.const_body, u with
-  | OpaqueDef _, `Opaque (b,c) ->
-      let pt = Future.from_val (b,c) in
-      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
-   | _ -> orig
-;;
-
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
+let turn_direct orig =
+  let cb = orig.seff_body in
+  if Declareops.is_opaque cb then
+    let p = match orig.seff_env with
+    | `Opaque (b, c) -> (b, c)
+    | _ -> assert false
+    in
+    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
+    let cb = { cb with const_body } in
+    { orig with seff_body = cb }
+  else orig
 
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
 
+let export_eff eff =
+  (eff.seff_constant, eff.seff_body, eff.seff_role)
+
 let export_side_effects mb env c =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = { c with
         const_entry_body = Future.chain body
           (fun (b_ctx, _) -> b_ctx, ()) } in
-      let not_exists (c,_,_,_) =
-        try ignore(Environ.lookup_constant c env); false
+      let not_exists e =
+        try ignore(Environ.lookup_constant e.seff_constant env); false
         with Not_found -> true in 
       let aux (acc,sl) { eff = se; from_env = mb } =
-        let cbl = match se with
-          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
-          | SEscheme (cl,k) ->
-              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
-        let cbl = List.filter not_exists cbl in
-        if cbl = [] then acc, sl
+        let cbl = List.filter not_exists se in
+        if List.is_empty cbl then acc, sl
         else cbl :: acc, (mb,List.length cbl) :: sl in
       let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
       let trusted = check_signatures mb signatures in
-      let push_seff env = function
-        | kn, cb, `Nothing, _ ->
-          begin
-            let env = Environ.add_constant kn cb env in
-            match cb.const_universes with
-            | Monomorphic_const ctx ->
-              Environ.push_context_set ~strict:true ctx env
-            | Polymorphic_const _ -> env
-          end
-        | kn, cb, `Opaque(_, ctx), _ ->
-          begin
-            let env = Environ.add_constant kn cb env in
-            match cb.const_universes with
-            | Monomorphic_const cstctx ->
-              let env = Environ.push_context_set ~strict:true cstctx env in
-              Environ.push_context_set ~strict:true ctx env
-            | Polymorphic_const _ -> env
-          end
+      let push_seff env eff =
+        let { seff_constant = kn; seff_body = cb } = eff in
+        let env = Environ.add_constant kn cb env in
+        match cb.const_universes with
+        | Polymorphic_const _ -> env
+        | Monomorphic_const ctx ->
+          let ctx = match eff.seff_env with
+          | `Nothing -> ctx
+          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          in
+          Environ.push_context_set ~strict:true ctx env
       in
       let rec translate_seff sl seff acc env =
         match seff with
@@ -527,18 +508,22 @@ let export_side_effects mb env c =
         | cbs :: rest ->
           if Int.equal sl 0 then
            let env, cbs =
-             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+             List.fold_left (fun (env,cbs) eff ->
+              let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in
                let ce = constant_entry_of_side_effect ocb u in
                let cb = translate_constant Pure env kn ce in
-               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) 
+               let eff = { eff with
+                seff_body = cb;
+                seff_env = `Nothing;
+               } in
+               (push_seff env eff, export_eff eff :: cbs))
              (env,[]) cbs in
            translate_seff 0 rest (cbs @ acc) env
           else
            let cbs_len = List.length cbs in
            let cbs = List.map turn_direct cbs in
            let env = List.fold_left push_seff env cbs in
-           let ecbs = List.map (fun (kn,cb,u,r) ->
-             kn, cb, r) cbs in
+           let ecbs = List.map export_eff cbs in
            translate_seff (sl - cbs_len) rest (ecbs @ acc) env
      in
        translate_seff trusted seff [] env
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6a0ff072f5..b05e05e4dc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -38,24 +38,18 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val empty_seff : side_effects
-val add_seff : side_effect -> side_effects -> side_effects
+val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects
 val concat_seff : side_effects -> side_effects -> side_effects
 (** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
     [e1] must be more recent than those of [e2]. *)
-val uniq_seff : side_effects -> side_effect list
+val uniq_seff : side_effects -> side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
-val equal_eff : side_effect -> side_effect -> bool
-
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
   
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 1c323e3ea2..60293fe864 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -62,6 +62,7 @@ type ('constr, 'types) ptype_error =
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.Constraint.t
+  | UndeclaredUniverse of Univ.Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -125,3 +126,6 @@ let error_elim_explain kp ki =
 
 let error_unsatisfied_constraints env c =
   raise (TypeError (env, UnsatisfiedConstraints c))
+
+let error_undeclared_universe env l =
+  raise (TypeError (env, UndeclaredUniverse l))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 20bf300ac3..9c6ef64b50 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -63,6 +63,7 @@ type ('constr, 'types) ptype_error =
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.Constraint.t
+  | UndeclaredUniverse of Univ.Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -108,3 +109,5 @@ val error_ill_typed_rec_body  :
 val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
 val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+
+val error_undeclared_universe : env -> Univ.Level.t -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7f36f3813f..25c1cbff3a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -431,7 +431,28 @@ and execute_recdef env (names,lar,vdef) i =
 and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
+
+let universe_levels_of_constr env c =
+  let rec aux s c =
+    match kind c with
+    | Const (c, u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Sort u when not (Sorts.is_small u) ->
+      let u = Sorts.univ_of_sort u in
+      LSet.fold LSet.add (Universe.levels u) s
+    | _ -> Constr.fold aux s c
+  in aux LSet.empty c
+
+let check_wellformed_universes env c =
+  let univs = universe_levels_of_constr env c in
+  try UGraph.check_declared_universes (universes env) univs
+  with UGraph.UndeclaredLevel u ->
+    error_undeclared_universe env u
+
 let infer env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
     make_judge constr t
 
@@ -449,11 +470,13 @@ let type_judgment env {uj_val=c; uj_type=t} =
   {utj_val = c; utj_type = s }
 
 let infer_type env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
 let infer_v env cv =
+  let () = Array.iter (check_wellformed_universes env) cv in
   let jv = execute_array env cv in
     make_judgev cv jv
 
@@ -461,9 +484,11 @@ let infer_v env cv =
 
 let infer_local_decl env id = function
   | Entries.LocalDefEntry c ->
+      let () = check_wellformed_universes env c in
       let t = execute env c in
       RelDecl.LocalDef (Name id, c, t)
   | Entries.LocalAssumEntry c ->
+      let () = check_wellformed_universes env c in
       let t = execute env c in
       RelDecl.LocalAssum (Name id, check_assumption env c t)
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index bc624ba56d..95d71965df 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -529,6 +529,11 @@ let add_universe vlev strict g =
 let add_universe_unconstrained vlev g =
   fst (add_universe_gen vlev g)
 
+exception UndeclaredLevel of Univ.Level.t
+let check_declared_universes g us =
+  let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in
+  Univ.LSet.iter check us
+
 exception Found_explanation of explanation
 
 let get_explanation strict u v g =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8c2d877b0b..752bf76270 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -55,6 +55,12 @@ val add_universe : Level.t -> bool -> t -> t
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
 
+(** Check that the universe levels are declared. Otherwise
+    @raise UndeclaredLevel l for the first undeclared level found. *)
+exception UndeclaredLevel of Univ.Level.t
+
+val check_declared_universes : t -> Univ.LSet.t -> unit
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t