Merge branch 'v8.5' into trunk

55 files changed, 657 insertions, 274 deletions

diff --git a/checker/values.ml b/checker/values.ml
index c986415070..cf93466b00 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -321,6 +321,33 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
 let v_libobjs = List v_libobj
 let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
 
+(** STM objects *)
+
+let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|])
+let v_states = v_pair Any v_frozen
+let v_state = Tuple ("state", [|v_states; Any; v_bool|])
+
+let v_vcs =
+  let data = Opt Any in
+  let vcs =
+    Tuple ("vcs",
+      [|Any; Any;
+        Tuple ("dag",
+          [|Any; Any; v_map Any (Tuple ("state_info",
+            [|Any; Any; Opt v_state; v_pair data Any|]))
+          |])
+      |])
+  in
+  let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in
+  vcs
+
+let v_uuid = Any
+let v_request id doc =
+  Tuple ("request", [|Any; Any; doc; Any; id; String|])
+let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool)
+let v_counters = Any
+let v_stm_seg = v_pair v_tasks v_counters
+
 (** Toplevel structures in a vo (see Cic.mli) *)
 
 let v_lib =
@@ -332,19 +359,19 @@ let v_univopaques =
 
 (** Registering dynamic values *)
 
-module StringOrd =
+module IntOrd =
 struct
-  type t = string
+  type t = int
   let compare (x : t) (y : t) = compare x y
 end
 
-module StringMap = Map.Make(StringOrd)
+module IntMap = Map.Make(IntOrd)
 
-let dyn_table : value StringMap.t ref = ref StringMap.empty
+let dyn_table : value IntMap.t ref = ref IntMap.empty
 
 let register_dyn name t =
-  dyn_table := StringMap.add name t !dyn_table
+  dyn_table := IntMap.add name t !dyn_table
 
 let find_dyn name =
-  try StringMap.find name !dyn_table
+  try IntMap.find name !dyn_table
   with Not_found -> Any
diff --git a/checker/votour.ml b/checker/votour.ml
index d016b45632..7c954d6f98 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,11 +10,44 @@ open Values
 
 (** {6 Interactive visit of a vo} *)
 
-(** Name of a value *)
-
-type dyn = { dyn_tag : string; dyn_obj : Obj.t; }
+type 'a repr =
+| INT of int
+| STRING of string
+| BLOCK of int * 'a array
+| OTHER
+
+module type S =
+sig
+  type obj
+  val input : in_channel -> obj
+  val repr : obj -> obj repr
+  val size : int list -> int
+end
+
+module Repr : S =
+struct
+  type obj = Obj.t
+
+  let input chan =
+    let obj = input_value chan in
+    let () = CObj.register_shared_size obj in
+    obj
+
+  let repr obj =
+    if Obj.is_block obj then
+      let tag = Obj.tag obj in
+      if tag = Obj.string_tag then STRING (Obj.magic obj)
+      else if tag < Obj.no_scan_tag then
+        let data = Obj.dup obj in
+        let () = Obj.set_tag data 0 in
+        BLOCK (tag, Obj.magic data)
+      else OTHER
+    else INT (Obj.magic obj)
+
+  let size p = CObj.shared_size_of_pos p
+end
 
-let to_dyn obj = (Obj.magic obj : dyn)
+(** Name of a value *)
 
 let rec get_name ?(extra=false) = function
   |Any -> "?"
@@ -32,69 +65,101 @@ let rec get_name ?(extra=false) = function
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
 
-let get_string_in_tuple v o =
+let get_string_in_tuple o =
   try
-    for i = 0 to Array.length v - 1 do
-      if v.(i) = String then
-        failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]");
+    for i = 0 to Array.length o - 1 do
+      match Repr.repr o.(i) with
+      | STRING s ->
+        failwith (Printf.sprintf " [..%s..]" s)
+      | _ -> ()
     done;
     ""
   with Failure s -> s
 
 (** Some details : tags, integer value for non-block, etc etc *)
 
-let rec get_details v o = match v with
-  |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) ->
-    " [" ^ String.escaped (Obj.magic o : string) ^"]"
-  |Tuple (_,v) -> get_string_in_tuple v o
-  |(Sum _|Any) when Obj.is_block o ->
-    " [tag=" ^ string_of_int (Obj.tag o) ^"]"
-  |(Sum _|Any) ->
-    " [imm=" ^ string_of_int (Obj.magic o : int) ^"]"
-  |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]"
-  |Annot (s,v) -> get_details v o
+let rec get_details v o = match v, Repr.repr o with
+  | (String | Any), STRING s ->
+    Printf.sprintf " [%s]" (String.escaped s)
+  |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o
+  |(Sum _|Any), BLOCK (tag, _) ->
+    Printf.sprintf " [tag=%i]" tag
+  |(Sum _|Any), INT i ->
+    Printf.sprintf " [imm=%i]" i
+  |Int, INT i -> Printf.sprintf " [imm=%i]" i
+  |Annot (s,v), _ -> get_details v o
   |_ -> ""
 
 let node_info (v,o,p) =
   get_name ~extra:true v ^ get_details v o ^
-    " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)"
+    " (size "^ string_of_int (Repr.size p)^"w)"
 
 (** Children of a block : type, object, position.
     For lists, we collect all elements of the list at once *)
 
-let access_children vs o pos =
-  Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs
-
+let access_children vs os pos =
+  if Array.length os = Array.length vs then
+    Array.mapi (fun i v -> v, os.(i), i::pos) vs
+  else raise Exit
+
+let access_list v o pos =
+  let rec loop o pos = match Repr.repr o with
+  | INT 0 -> []
+  | BLOCK (0, [|hd; tl|]) ->
+    (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+  | _ -> raise Exit
+  in
+  Array.of_list (loop o pos)
+
+let access_block o = match Repr.repr o with
+| BLOCK (tag, os) -> (tag, os)
+| _ -> raise Exit
+let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
+
+(** raises Exit if the object has not the expected structure *)
 let rec get_children v o pos = match v with
-  |Tuple (_,v) -> access_children v o pos
-  |Sum (_,_,vv) ->
-    if Obj.is_block o then access_children vv.(Obj.tag o) o pos
-    else [||]
-  |Array v -> access_children (Array.make (Obj.size o) v) o pos
-  |List v ->
-    let rec loop pos = function
-      | [] -> []
-      | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol
-    in
-    Array.of_list (loop pos (Obj.magic o : Obj.t list))
+  |Tuple (_, v) ->
+    let (_, os) = access_block o in
+    access_children v os pos
+  |Sum (_, _, vv) ->
+    begin match Repr.repr o with
+    | BLOCK (tag, os) -> access_children vv.(tag) os pos
+    | INT _ -> [||]
+    | _ -> raise Exit
+    end
+  |Array v ->
+    let (_, os) = access_block o in
+    access_children (Array.make (Array.length os) v) os pos
+  |List v -> access_list v o pos
   |Opt v ->
-    if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||]
+    begin match Repr.repr o with
+    | INT 0 -> [||]
+    | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
+    | _ -> raise Exit
+    end
   |String | Int -> [||]
   |Annot (s,v) -> get_children v o pos
-  |Any ->
-    if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then
-      Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos))
-    else [||]
+  |Any -> raise Exit
   |Dyn ->
-    let t = to_dyn o in
-    let tpe = find_dyn t.dyn_tag in
-    [|(Int, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|]
+    begin match Repr.repr o with
+    | BLOCK (0, [|id; o|]) ->
+      let n = access_int id in
+      let tpe = find_dyn n in
+      [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
+    | _ -> raise Exit
+    end
   |Fail s -> failwith "forbidden"
 
+let get_children v o pos =
+  try get_children v o pos
+  with Exit -> match Repr.repr o with
+  | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os
+  | _ -> [||]
+
 type info = {
   nam : string;
   typ : value;
-  obj : Obj.t;
+  obj : Repr.obj;
   pos : int list
 }
 
@@ -154,7 +219,7 @@ let visit_vo f =
     {name="library"; pos=0; typ=Values.v_lib};
     {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; 
     {name="discharging info"; pos=0; typ=Opt Any};
-    {name="STM tasks"; pos=0; typ=Opt Any};
+    {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg};
     {name="opaque proofs"; pos=0; typ=Values.v_opaques}; 
   |] in
   while true do
@@ -176,8 +241,7 @@ let visit_vo f =
     let l = read_line () in
     let seg = int_of_string l in
     seek_in ch segments.(seg).pos;
-    let o = (input_value ch : Obj.t) in
-    let () = CObj.register_shared_size o in
+    let o = Repr.input ch in
     let () = init () in
     visit segments.(seg).typ o []
   done
diff --git a/configure.ml b/configure.ml
index e8ef3ace7f..3cf462ebe0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -17,7 +17,7 @@ three non-negative, period-separed integers [...]" *)
 let vo_magic = 8511
 let state_magic = 58511
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
-"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert"]
+"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
 
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 3f232c3612..a7241399e0 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 
 let wit_bindings = unsafe_of_type BindingsArgType
 
+let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
+  Genarg.make0 None "hyp_location_flag"
+
 let wit_red_expr = unsafe_of_type RedExprArgType
 
 let wit_clause_dft_concl  =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 74c6bd310c..fdeddd66a1 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -64,6 +64,8 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings Evd.sigma) genarg_type
 
+val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
+
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/interp/notation.ml b/interp/notation.ml
index aeec4b6153..80db2cb396 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -136,10 +136,6 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
   if Int.equal i 1 then
-    let sc = match sc with
-      | Scope sc -> Scope (normalize_scope sc)
-      | _ -> sc
-    in
     scope_stack :=
       if op then sc :: !scope_stack
       else List.except scope_eq sc !scope_stack
@@ -166,7 +162,7 @@ let inScope : bool * bool * scope_elem -> obj =
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
+  Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
 
 let empty_scope_stack = []
 
@@ -516,6 +512,32 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 (* Miscellaneous *)
 
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+
+let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
+  Id.equal id1 id2 &&
+  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1) (vars2, t2) =
+  List.equal vars_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr t1 t2
+
+let exists_notation_in_scope scopt ntn r =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = String.Map.find scope !scope_map in
+    let (r',_) = String.Map.find ntn sc.notations in
+    interpretation_eq r' r
+  with Not_found -> false
+
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
diff --git a/interp/notation.mli b/interp/notation.mli
index c66115cbdd..854c52b2c7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
+(** Checks for already existing notations *)
+val exists_notation_in_scope : scope_name option -> notation ->
+      interpretation -> bool
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> global_reference -> scope_name option list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c91c781591..2762dc0b8d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -170,6 +170,69 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
 
 let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
 
+let rec eq_notation_constr t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Id.equal id1 id2
+| NApp (t1, a1), NApp (t2, a2) ->
+  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+  let eqpat (p1, t1) (p2, t2) =
+    List.equal cases_pattern_eq p1 p2 &&
+    eq_notation_constr t1 t2
+  in
+  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
+    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+  in
+  Option.equal eq_notation_constr o1 o2 &&
+  List.equal eqf r1 r2 &&
+  List.equal eqpat p1 p2
+| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+  List.equal Name.equal nas1 nas2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+  eq_notation_constr t1 t2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr u1 u2 &&
+  eq_notation_constr r1 r2
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+  let eq (na1, o1, t1) (na2, o2, t2) =
+    Name.equal na1 na2 &&
+    Option.equal eq_notation_constr o1 o2 &&
+    eq_notation_constr t1 t2
+  in
+  Array.equal Id.equal ids1 ids2 &&
+  Array.equal (List.equal eq) ts1 ts2 &&
+  Array.equal eq_notation_constr us1 us2 &&
+  Array.equal eq_notation_constr rs1 rs2
+| NSort s1, NSort s2 ->
+  Miscops.glob_sort_eq s1 s2
+| NPatVar p1, NPatVar p2 ->
+  Id.equal p1 p2
+| NCast (t1, c1), NCast (t2, c2) ->
+  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+  | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false
+
+
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 7283ed6f12..c6770deea2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -25,6 +25,8 @@ val ldots_var : Id.t
 (** FIXME: nothing to do here *)
 val eq_glob_constr : glob_constr -> glob_constr -> bool
 
+val eq_notation_constr : notation_constr -> notation_constr -> bool
+
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 07891d0b48..450b1af0f9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -316,7 +316,7 @@ type vernac_expr =
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
-      export_flag option * lreference list
+      lreference option * export_flag option * lreference list
   | VernacImport of export_flag * lreference list
   | VernacCanonical of reference or_by_notation
   | VernacCoercion of obsolete_locality * reference or_by_notation *
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 52dc49bf8e..1be3e65113 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) {
       uint32_t i, sizes, const_size, block_size;
       COPY32(q,p); p++;
       sizes=*q++;
-      const_size = sizes & 0xFFFF;
-      block_size = sizes >> 16;
+      const_size = sizes & 0xFFFFFF;
+      block_size = sizes >> 24;
       sizes = const_size + block_size;
       for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
     } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d74affdea9..0ab9f89ffa 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -791,12 +791,12 @@ value coq_interprete
       Instruct(SWITCH) {
 	uint32_t sizes = *pc++;
 	print_instr("SWITCH");
-	print_int(sizes & 0xFFFF);
+	print_int(sizes & 0xFFFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ae679027d6..700de50200 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,6 +24,9 @@ let fix_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
+(* It could be greate if OCaml export this value,
+   So fixme if this occur in a new version of OCaml *)
+let last_variant_tag = 245 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index b65268f722..fbb40ffd1f 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -20,6 +20,7 @@ val fix_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
+val last_variant_tag : tag 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 3b0c93b322..07fab06a42 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -329,13 +329,50 @@ let init_fun_code () = fun_code := []
 
 (* Compilation of constructors and inductive types *)
 
+
+(* Limitation due to OCaml's representation of non-constant
+  constructors: limited to 245 + 1 (0 tag) cases. *)
+
+exception TooLargeInductive of Id.t
+
+let max_nb_const = 0x1000000 
+let max_nb_block = 0x1000000 + last_variant_tag - 1
+
+let str_max_constructors = 
+  Format.sprintf 
+    " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
+
+let check_compilable ib = 
+  
+  if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then 
+    raise (TooLargeInductive ib.mind_typename)
+
+(* Inv: arity > 0 *)
+
+let const_bn tag args = 
+  if tag < last_variant_tag then Const_bn(tag, args)
+  else
+    Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
+
+  
+let code_makeblock arity tag cont = 
+  if tag < last_variant_tag then
+    Kmakeblock(arity, tag) :: cont
+  else
+    Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) ::
+    Kmakeblock(arity+1, last_variant_tag) :: cont
+
 (* Inv : nparam + arity > 0 *)
 let code_construct tag nparams arity cont =
   let f_cont =
       add_pop nparams
       (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
-       else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
+       else if tag < last_variant_tag then
+         [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
+       else 
+         [Kconst (Const_b0 (tag - last_variant_tag)); 
+          Kmakeblock(arity+1, last_variant_tag); Kreturn 0])
     in
     let lbl = Label.create() in
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
@@ -345,7 +382,6 @@ let get_strcst = function
   | Bstrconst sc -> sc
   | _ -> raise Not_found
 
-
 let rec str_const c =
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
@@ -357,7 +393,8 @@ let rec str_const c =
             begin
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
-	    let num,arity = oip.mind_reloc_tbl.(i-1) in
+	    let () = check_compilable oip in
+	    let tag,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if Int.equal (nparams + arity) (Array.length args) then
               (* spiwack: *)
@@ -399,15 +436,15 @@ let rec str_const c =
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
 		      falls back to the normal behavior *)
-		if Int.equal arity 0 then Bstrconst(Const_b0 num)
+		if Int.equal arity 0 then Bstrconst(Const_b0 tag)
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
 		  try
 		    let sc_args = Array.map get_strcst b_args in
-		    Bstrconst(Const_bn(num, sc_args))
+		    Bstrconst(const_bn tag sc_args)
 		  with Not_found ->
-		    Bmakeblock(num,b_args)
+		    Bmakeblock(tag,b_args)
 	    else
               let b_args = Array.map str_const args in
 	     (* spiwack: tries first to apply the run-time compilation
@@ -418,7 +455,7 @@ let rec str_const c =
                                            f),
                          b_args)
 	      with Not_found ->
-	        Bconstruct_app(num, nparams, arity, b_args)
+	        Bconstruct_app(tag, nparams, arity, b_args)
               end
 	| _ -> Bconstr c
       end
@@ -435,6 +472,7 @@ let rec str_const c =
       with Not_found ->
 	let oib = lookup_mind kn !global_env in
 	let oip = oib.mind_packets.(j) in
+	let () = check_compilable oip in
 	let num,arity = oip.mind_reloc_tbl.(i-1) in
 	let nparams = oib.mind_nparams in
 	if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
@@ -489,9 +527,12 @@ let rec compile_fv reloc l sz cont =
 let rec get_allias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
-    (match Cemitcodes.force tps with
-    | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
-    | _ -> p)
+    match tps with
+    | None -> p
+    | Some tps ->
+       (match Cemitcodes.force tps with
+	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+	| _ -> p)
 
 (* Compiling expressions *)
 
@@ -607,9 +648,14 @@ let rec compile_constr reloc c sz cont =
       let ind = ci.ci_ind in
       let mib = lookup_mind (fst ind) !global_env in
       let oib = mib.mind_packets.(snd ind) in
+      let () = check_compilable oib in
       let tbl = oib.mind_reloc_tbl in
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
-      let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in
+      let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+      let nblock = min nallblock (last_variant_tag + 1) in
+      let lbl_blocks = Array.make nblock Label.no in
+      let neblock = max 0 (nallblock - last_variant_tag) in
+      let lbl_eblocks = Array.make neblock Label.no in 
       let branch1,cont = make_branch cont in
       (* Compiling return type *)
       let lbl_typ,fcode =
@@ -629,6 +675,15 @@ let rec compile_constr reloc c sz cont =
       in
       lbl_blocks.(0) <- lbl_accu;
       let c = ref code_accu in
+      (* perform the extra match if needed (to many block constructors) *)
+      if neblock <> 0 then begin
+        let lbl_b, code_b = 
+          label_code (
+            Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
+        lbl_blocks.(last_variant_tag) <- lbl_b;
+        c := code_b
+      end;  
+      
       (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
@@ -640,22 +695,24 @@ let rec compile_constr reloc c sz cont =
 	else
 	  let args, body = decompose_lam branchs.(i) in
 	  let nargs = List.length args in
-	  let lbl_b,code_b =
-	    label_code(
-	    if Int.equal nargs arity then
-	      Kpushfields arity ::
+         
+          let code_b =  
+            if Int.equal nargs arity then
 	      compile_constr (push_param arity sz_b reloc)
 		body (sz_b+arity) (add_pop arity (branch :: !c))
 	    else
 	      let sz_appterm = if is_tailcall then sz_b + arity else arity in
-	      Kpushfields arity ::
 	      compile_constr reloc branchs.(i) (sz_b+arity)
-		(Kappterm(arity,sz_appterm) :: !c))
-	  in
-	  lbl_blocks.(tag) <- lbl_b;
+		(Kappterm(arity,sz_appterm) :: !c) in
+          let code_b = 
+            if tag < last_variant_tag then Kpushfields arity :: code_b
+            else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in
+          let lbl_b,code_b = label_code code_b in
+          if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
+          else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
 	  c := code_b
       done;
-      c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
+      c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
       let code_sw =
  	match branch1 with
         (* spiwack : branch1 can't be a lbl anymore it's a Branch instead
@@ -677,9 +734,10 @@ and compile_str_cst reloc sc sz cont =
   | Bstrconst sc -> Kconst sc :: cont
   | Bmakeblock(tag,args) ->
       let nargs = Array.length args in
-      comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
+      comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
+      if Int.equal (Array.length args) 0 then
+        code_construct tag nparams arity cont
       else
 	comp_app
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -706,13 +764,14 @@ and compile_const =
                    Kgetglobal (get_allias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
-let compile env c =
+let compile fail_on_error env c =
   set_global_env env;
   init_fun_code ();
   Label.reset_label_counter ();
   let reloc = empty_comp_env () in
-  let init_code = compile_constr reloc c 0 [Kstop] in
-  let fv = List.rev (!(reloc.in_env).fv_rev) in
+  try 
+    let init_code = compile_constr reloc c 0 [Kstop] in
+    let fv = List.rev (!(reloc.in_env).fv_rev) in
 (*  draw_instr init_code;
   draw_instr !fun_code;
   Format.print_string "fv = ";
@@ -722,21 +781,26 @@ let compile env c =
     | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv;  Format
     .print_string "\n";
   Format.print_flush();  *)
-  init_code,!fun_code, Array.of_list fv
-
-let compile_constant_body env = function
-  | Undef _ | OpaqueDef _ -> BCconstant
+      Some (init_code,!fun_code, Array.of_list fv)
+  with TooLargeInductive tname ->
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+      (Pp.(fn
+	   (str "Cannot compile code for virtual machine as it uses inductive " ++
+	    Id.print tname ++ str str_max_constructors));
+       None)
+
+let compile_constant_body fail_on_error env = function
+  | Undef _ | OpaqueDef _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
       match kind_of_term body with
 	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      BCallias (get_allias env (con,u))
+	      Some (BCallias (get_allias env (con,u)))
 	| _ ->
-	    let res = compile env body in
-	    let to_patch = to_memory res in
-	    BCdefined to_patch
+	    let res = compile fail_on_error env body in
+	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 8fb6601a93..1128f0d0b7 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -5,10 +5,12 @@ open Declarations
 open Pre_env
 
 
-val compile : env -> constr -> bytecodes * bytecodes * fv
-                              (** init, fun, fv *)
+val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
+	      env -> constr -> (bytecodes * bytecodes * fv) option
+(** init, fun, fv *)
 
-val compile_constant_body : env -> constant_def -> body_code
+val compile_constant_body : bool -> 
+			    env -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 9ecae2b36f..2535a64d3c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -23,34 +23,22 @@ type reloc_info =
 
 type patch = reloc_info * int
 
+let patch_char4 buff pos c1 c2 c3 c4 = 
+  String.unsafe_set buff pos       c1;
+  String.unsafe_set buff (pos + 1) c2;
+  String.unsafe_set buff (pos + 2) c3;
+  String.unsafe_set buff (pos + 3) c4 
+  
 let patch_int buff pos n =
-  String.unsafe_set buff pos (Char.unsafe_chr n);
-  String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
-  String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
-  String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
-
+  patch_char4 buff pos 
+    (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
+    (Char.unsafe_chr (n asr 24))
 
 (* Buffering of bytecode *)
 
 let out_buffer = ref(String.create 1024)
 and out_position = ref 0
 
-(*
-let out_word b1 b2 b3 b4 =
-  let p = !out_position in
-  if p >= String.length !out_buffer then begin
-    let len = String.length !out_buffer in
-    let new_buffer = String.create (2 * len) in
-    String.blit !out_buffer 0 new_buffer 0 len;
-    out_buffer := new_buffer
-  end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
-  out_position := p + 4
-*)
-
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
   if p >= String.length !out_buffer then begin
@@ -66,13 +54,10 @@ let out_word b1 b2 b3 b4 =
     String.blit !out_buffer 0 new_buffer 0 len;
     out_buffer := new_buffer
   end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  patch_char4 !out_buffer p (Char.unsafe_chr b1)
+   (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
   out_position := p + 4
 
-
 let out opcode =
   out_word opcode 0 0 0
 
@@ -101,7 +86,7 @@ let extend_label_table needed =
 
 let backpatch (pos, orig) =
   let displ = (!out_position - orig) asr 2 in
-  !out_buffer.[pos] <- Char.unsafe_chr displ;
+  !out_buffer.[pos]   <- Char.unsafe_chr displ;
   !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
   !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
   !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
@@ -222,8 +207,12 @@ let emit_instr = function
       out_label typlbl; out_label swlbl;
       slot_for_annot annot;out_int sz
   | Kswitch (tbl_const, tbl_block) ->
+      let lenb = Array.length tbl_block in
+      let lenc = Array.length tbl_const in
+      assert (lenb < 0x100 && lenc < 0x1000000);
       out opSWITCH;
-      out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+      out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
+(*      out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
       let org = !out_position in
       Array.iter (out_label_with_orig org) tbl_const;
       Array.iter (out_label_with_orig org) tbl_block
@@ -333,25 +322,41 @@ let subst_patch s (ri,pos) =
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
+let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
+
 type body_code =
   | BCdefined of to_patch
   | BCallias of pconstant
   | BCconstant
 
-let subst_body_code s = function
-  | BCdefined tp -> BCdefined (subst_to_patch s tp)
-  | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
-  | BCconstant -> BCconstant
-
-type to_patch_substituted = body_code substituted
-
-let from_val = from_val
-
-let force = force subst_body_code
-
-let subst_to_patch_subst = subst_substituted
-
-let repr_body_code = repr_substituted
+type to_patch_substituted =
+| PBCdefined of to_patch substituted
+| PBCallias of pconstant substituted
+| PBCconstant
+
+let from_val = function
+| BCdefined tp -> PBCdefined (from_val tp)
+| BCallias cu -> PBCallias (from_val cu)
+| BCconstant -> PBCconstant
+
+let force = function
+| PBCdefined tp -> BCdefined (force subst_to_patch tp)
+| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCconstant -> BCconstant
+
+let subst_to_patch_subst s = function
+| PBCdefined tp -> PBCdefined (subst_substituted s tp)
+| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCconstant -> PBCconstant
+
+let repr_body_code = function
+| PBCdefined tp ->
+  let (s, tp) = repr_substituted tp in
+  (s, BCdefined tp)
+| PBCallias cu ->
+  let (s, cu) = repr_substituted cu in
+  (s, BCallias cu)
+| PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
   init();
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index ed8b0a6d1d..b29f06c652 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) =
   with NotEvaluated ->
 (*    Pp.msgnl(str"not yet evaluated");*)
     let pos =
-      match Cemitcodes.force cb.const_body_code with
-      | BCdefined(code,pl,fv) ->
-	if Univ.Instance.is_empty u then
-	  let v = eval_to_patch env (code,pl,fv) in
-	    set_global v
-	else set_global (val_of_constant (kn,u))
-    | BCallias kn' -> slot_for_getglobal env kn'
-    | BCconstant -> set_global (val_of_constant (kn,u)) in
+      match cb.const_body_code with
+      | None -> set_global (val_of_constant (kn,u))
+      | Some code ->
+	 match Cemitcodes.force code with
+	 | BCdefined(code,pl,fv) ->
+	    if Univ.Instance.is_empty u then
+	    let v = eval_to_patch env (code,pl,fv) in
+	      set_global v
+	    else set_global (val_of_constant (kn,u))
+	 | BCallias kn' -> slot_for_getglobal env kn'
+	 | BCconstant -> set_global (val_of_constant (kn,u)) in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
     pos
@@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) =
 
 and val_of_constr env c =
   let (_,fun_code,_ as ccfv) =
-    try compile env c
+    try match compile true env c with
+	| Some v -> v
+	| None -> assert false
     with reraise ->
       let reraise = Errors.push reraise in
       let () = print_string "can not compile \n" in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index cef920c6a5..27c1c3f3f0 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -70,7 +70,7 @@ type constant_body = {
     const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
-    const_body_code : Cemitcodes.to_patch_substituted;
+    const_body_code : Cemitcodes.to_patch_substituted option;
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
@@ -139,7 +139,7 @@ type one_inductive_body = {
 
     mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
-    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
+    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
  (** Number of expected proper arguments of the constructors (w/o params)
@@ -172,7 +172,7 @@ type mutual_inductive_body = {
 
     mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
 
-    mind_nparams : int;  (** Number of expected parameters *)
+    mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 48a6098eee..a7051d5c13 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -129,7 +129,7 @@ let subst_const_body sub cb =
         const_type = type';
         const_proj = proj';
         const_body_code =
-          Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+          Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0ebff440a1..a79abbb7e8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -473,7 +473,7 @@ type unsafe_type_judgment = {
 
 (*s Compilation of global declaration *)
 
-let compile_constant_body = Cbytegen.compile_constant_body
+let compile_constant_body = Cbytegen.compile_constant_body false
 
 exception Hyp_not_found
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index de960ecccf..ede356e699 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -253,7 +253,7 @@ type unsafe_type_judgment = {
 
 (** {6 Compilation of global declaration } *)
 
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code
+val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
 
 exception Hyp_not_found
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 799471c68a..6b909824ba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -346,7 +346,7 @@ let typecheck_inductive env mie =
       in
 	(id,cn,lc,(sign,arity)))
     inds
-  in (env_arities, params, inds)
+  in (env_arities, env_ar_par, params, inds)
 
 (************************************************************************)
 (************************************************************************)
@@ -366,9 +366,8 @@ exception IllFormedInd of ill_formed_ind
 
 let mind_extract_params = decompose_prod_n_assum
 
-let explain_ind_err id ntyp env0 nbpar c nargs err =
+let explain_ind_err id ntyp env nbpar c nargs err =
   let (lpar,c') = mind_extract_params nbpar c in
-  let env = push_rel_context lpar env0 in
   match err with
     | LocalNonPos kt ->
 	raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
@@ -486,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	          check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
 	| Rel k ->
             (try let (ra,rarg) = List.nth ra_env (k-1) in
+            let largs = List.map (whd_betadeltaiota env) largs in
 	    let nmr1 =
 	      (match ra with
                   Mrec _ -> compute_rec_par ienv hyps nmr largs
@@ -822,9 +822,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar, params, inds) = typecheck_inductive env mie in
+  let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 99d353aae6..26dd45f5f3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -97,7 +97,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
+	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
 	  const_universes = ctx' }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d8f319fa79..d52fe611c0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver =
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) }
+	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 543397df53..383f810295 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -375,9 +375,12 @@ let makeblock env cn u tag args =
 
 let rec get_allias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
-  match Cemitcodes.force tps with
-  |  Cemitcodes.BCallias kn' -> get_allias env kn'
-  | _ -> p
+    match tps with
+    | None -> p
+    | Some tps ->
+       match Cemitcodes.force tps with
+       | Cemitcodes.BCallias kn' -> get_allias env kn'
+       | _ -> p
 
 (*i Global environment *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b54511e402..a316b4492b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -245,12 +245,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
   let tps = 
     (* FIXME: incompleteness of the bytecode vm: we compile polymorphic 
        constants like opaque definitions. *)
-    if poly then Cemitcodes.from_val Cemitcodes.BCconstant
+    if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
     else
-      match proj with
-      | None -> Cemitcodes.from_val (compile_constant_body env def)
-      | Some pb ->
-	Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
+      let res = 
+	match proj with
+	| None -> compile_constant_body env def
+	| Some pb ->
+	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+      in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 29315b0a90..1c31cc0414 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -64,8 +64,9 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vconstr_const i1, Vconstr_const i2 ->
       if Int.equal i1 i2 then cu else raise NotConvertible
   | Vconstr_block b1, Vconstr_block b2 ->
+      let tag1 = btag b1 and tag2 = btag b2 in
       let sz = bsize b1 in
-      if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
+      if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
 	  rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 2cc1efe431..d4bf461b39 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -79,7 +79,7 @@ type vprod
 type vfun
 type vfix
 type vcofix
-type vblock
+type vblock 
 type arguments
 
 type vm_env
@@ -224,10 +224,9 @@ let whd_val : values -> whd =
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
 	   | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
-	else Vconstr_block(Obj.obj o)
-
-
-
+	else 
+          Vconstr_block(Obj.obj o)
+         
 (************************************************)
 (* Abstrct machine ******************************)
 (************************************************)
@@ -518,8 +517,13 @@ let type_of_switch sw =
 let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
-    let b = Obj.new_block tag arity in
-    for i = 0 to arity - 1 do
+    let b, ofs = 
+      if tag < last_variant_tag then Obj.new_block tag arity, 0
+      else
+        let b = Obj.new_block last_variant_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        b,1 in
+    for i = ofs to ofs + arity - 1 do
       Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
     done;
     val_of_obj b
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 295ea83c49..5190356828 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -94,7 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array
 
 (** Block *)
 
-val btag : vblock -> int
+val btag  : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
diff --git a/library/summary.ml b/library/summary.ml
index 7e7628a1b7..8e2abbf15b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -66,6 +66,7 @@ let freeze_summaries ~marshallable : frozen =
   let fold id (_, decl) accu =
     (* to debug missing Lazy.force
     if marshallable <> `No then begin
+      let id, _ = Int.Map.find id !summaries in
       prerr_endline ("begin marshalling " ^ id);
       ignore(Marshal.to_string (decl.freeze_function marshallable) []);
       prerr_endline ("end marshalling " ^ id);
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 3cd7dbc9be..a4dba506d2 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -33,7 +33,7 @@ let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          constr_may_eval;
+          constr_may_eval constr_eval;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b42b2c6dd3..69593f993c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -202,7 +202,7 @@ let merge_occurrences loc cl = function
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl;
+  simple_intropattern clause_dft_concl hypident;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 70a8ec5522..cf7f6af28b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -465,11 +465,10 @@ GEXTEND Gram
 
       (* Requiring an already compiled module *)
       | IDENT "Require"; export = export_token; qidl = LIST1 global ->
-          VernacRequire (export, qidl)
+          VernacRequire (None, export, qidl)
       | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
 	; qidl = LIST1 global ->
-	let qidl = List.map (Libnames.join_reference ns) qidl in
-	VernacRequire (export, qidl)
+	VernacRequire (Some ns, export, qidl)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cf6435fec4..54edbb2c88 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -375,7 +375,9 @@ module Tactic =
       make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
     let bindings =
       make_gen_entry utactic (rawwit wit_bindings) "bindings"
+    let hypident = Gram.entry_create "hypident"
     let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
+    let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
     let uconstr =
       make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
     let quantified_hypothesis =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index dbd2aadf9d..2146ad964f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -215,7 +215,9 @@ module Tactic :
     val open_constr : open_constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
+    val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
     val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+    val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
     val uconstr : constr_expr Gram.entry
     val quantified_hypothesis : quantified_hypothesis Gram.entry
     val int_or_var : int or_var Gram.entry
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 80167686aa..deaf603ef0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,10 +274,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
+    let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      (*FIXME*) Evd.empty
+      evd
     new_principle_type
       hook
     ;
@@ -323,7 +324,7 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
+	let ce = Declare.definition_entry value in 
 	ignore(
 	  Declare.declare_constant
 	    name
@@ -447,7 +448,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   let first_fun = List.hd funs in
 
 
-  let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+  let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical first_fun) in
   let first_fun_kn =
     try
       fst (find_Function_infos  first_fun).graph_ind
@@ -498,27 +499,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
 	(fun _ _ _ -> ())
-  with e when Errors.noncritical e ->
-    begin
-      begin
-	try
-	  let id = Pfedit.get_current_proof_name () in
-	  let s = Id.to_string id in
-	  let n = String.length "___________princ_________" in
-	  if String.length s >= n
-	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Pfedit.delete_current_proof ()
-	  else ()
-	  else ()
-	with e when Errors.noncritical e -> ()
-      end;
-      raise (Defining_principle e)
-    end
+    with e when Errors.noncritical e ->
+       begin
+	 begin
+	   try
+	     let id = Pfedit.get_current_proof_name () in
+	     let s = Id.to_string id in
+	     let n = String.length "___________princ_________" in
+	     if String.length s >= n
+	     then if String.equal (String.sub s 0 n) "___________princ_________"
+		  then Pfedit.delete_current_proof ()
+		  else ()
+	     else ()
+	   with e when Errors.noncritical e -> ()
+	 end;
+	 raise (Defining_principle e)
+       end
 
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos this_block_funs.(0) in
+    let finfos = find_Function_infos first_fun in
     try
       let equation =  Option.get finfos.equation_lemma in
       Declareops.is_opaque (Global.lookup_constant equation)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 559f5fe66a..055996de55 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2
-  | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
+  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
 module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index cf6ac619dd..161cffa865 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,34 +351,45 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next =
     else mkresult subst (mk_ctx (mkMeta special_meta)) next
   with PatternMatchingFailure -> next ()
 
+let subargs env v = Array.map_to_list (fun c -> (env, c)) v
+
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let rec aux env c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
-      let next () = try_aux [env] [c1] next_mk_ctx next in
+      let next_mk_ctx = function
+      | [c1] -> mk_ctx (mkCast (c1, k, c2))
+      | _ -> assert false
+      in
+      let next () = try_aux [env, c1] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Lambda (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1; c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Prod (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
-      | [c1;c2] -> mkLetIn (x,c1,t,c2)
+      | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
       let next () = 
 	let env' = Environ.push_rel (x,Some c1,t) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | App (c1,lc) ->
       let next () =
@@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             let mk_ctx = function
               | [app';c] -> mk_ctx (mkApp (app',[|c|]))
               | _ -> assert false in
-            try_aux [env] [app;Array.last lc] mk_ctx next
+            try_aux [(env, app); (env, Array.last lc)] mk_ctx next
           else
             let rec aux2 app args next =
               match args with
               | [] ->
                   let mk_ctx le =
                     mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-                  try_aux [env] (c1::Array.to_list lc) mk_ctx next
+                  let sub = (env, c1) :: subargs env lc in
+                  try_aux sub mk_ctx next
               | arg :: args ->
                   let app = mkApp (app,[|arg|]) in
                   let next () = aux2 app args next in
@@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
         else
           let mk_ctx le =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-          try_aux [env] (c1::Array.to_list lc) mk_ctx next
+          let sub = (env, c1) :: subargs env lc in
+          try_aux sub mk_ctx next
       in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Case (ci,hd,c1,lc) ->
@@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in
+      let sub = (env, c1) :: subargs env lc in
+      let next () = try_aux sub next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux
-	[env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | CoFix (i,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
@@ -443,25 +456,22 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
 	    aux env term mk_ctx next
 	with Retyping.RetypeError _ -> next ()
       else
-	try_aux [env] [c'] next_mk_ctx next in
+      try_aux [env, c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ env sigma partial_app closed pat c mk_ctx next
 
   (* Tries [sub_match] for all terms in the list *)
-  and try_aux lenv lc mk_ctx next =
-    let rec try_sub_match_rec lacc lenv lc = 
-      match lenv, lc with
-      | _, [] -> next ()
-      | env :: tlenv, c::tl ->
-          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
-          let next () = 
-	    let env' = match tlenv with [] -> lenv | _ -> tlenv in
-	      try_sub_match_rec (c::lacc) env' tl 
-	  in
-            aux env c mk_ctx next 
-      | _ -> assert false in
-    try_sub_match_rec [] lenv lc in
+  and try_aux lc mk_ctx next =
+    let rec try_sub_match_rec lacc lc =
+      match lc with
+      | [] -> next ()
+      | (env, c) :: tl ->
+        let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
+        let next () = try_sub_match_rec (c :: lacc) tl in
+        aux env c mk_ctx next
+    in
+    try_sub_match_rec [] lc in
   let lempty () = IStream.Nil in
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb4169..e514fd529e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
+val cast_type_eq : ('a -> 'a -> bool) ->
+  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
 val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7f6a4a6442..dfdc24d480 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -365,14 +365,16 @@ let get_arity env ((ind,u),params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let parsign =
     (* Dynamically detect if called with an instance of recursively
-       uniform parameter only or also of non recursively uniform
+       uniform parameter only or also of recursively non-uniform
        parameters *)
-    let parsign = mib.mind_params_ctxt in
-    let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
-    if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
-      snd (List.chop nnonrecparams mib.mind_params_ctxt)
-    else
-      parsign in
+    let nparams = List.length params in
+    if Int.equal nparams mib.mind_nparams then
+      mib.mind_params_ctxt
+    else begin
+      assert (Int.equal nparams mib.mind_nparams_rec);
+      let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
+      snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+    end in
   let parsign = Vars.subst_instance_context u parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index af1783b705..7959759a3f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array
 (** Return constructor types in normal form *)
 val arities_of_constructors : env -> pinductive -> types array
 
-(** An inductive type with its parameters *)
+(** An inductive type with its parameters (transparently supports
+    reasoning either with only recursively uniform parameters or with all
+    parameters including the recursively non-uniform ones *)
 type inductive_family
 val make_ind_family : inductive puniverses * constr list -> inductive_family
 val dest_ind_family : inductive_family -> inductive puniverses * constr list
@@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
-val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
 val get_projections  : env -> inductive_family -> constant array option
 
+(** [get_arity] returns the arity of the inductive family instantiated
+    with the parameters; if recursively non-uniform parameters are not
+    part of the inductive family, they appears in the arity *)
+val get_arity        : env -> inductive_family -> rel_context * sorts_family
+
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 19613c4e06..8198db1b8a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -166,8 +166,15 @@ and nf_whd env whd typ =
       mkApp(cfd,args)
   | Vconstr_const n -> construct_of_constr_const env n typ
   | Vconstr_block b ->
-      let capp,ctyp = construct_of_constr_block env (btag b) typ in
-      let args = nf_bargs env b ctyp in
+      let tag = btag b in
+      let (tag,ofs) =
+        if tag = Cbytecodes.last_variant_tag then
+	  match whd_val (bfield b 0) with
+	  | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+	  | _ -> assert false
+        else (tag, 0) in
+      let capp,ctyp = construct_of_constr_block env tag typ in
+      let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
 	t := subst1 c codom; c) in
   !t,args
 
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
   let t = ref t in
-  let len = bsize b in
+  let len = bsize b - ofs in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (bfield b i) dom in
+	let c = nf_val env (bfield b (i+ofs)) dom in
 	t := subst1 c codom; c) in
   args
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e0b94669c2..89ffae4b3e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -863,10 +863,14 @@ module Make
         | VernacNameSectionHypSet (id,set) ->
           return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
           str ":="++spc()++pr_using set))
-        | VernacRequire (exp, l) ->
+        | VernacRequire (from, exp, l) ->
+          let from = match from with
+          | None -> mt ()
+          | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+          in
           return (
             hov 2
-              (keyword "Require" ++ spc() ++ pr_require_token exp ++
+              (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
                  prlist_with_sep sep pr_module l)
           )
         | VernacImport (f,l) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index d9ecc8bcce..477ca1f0dc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1093,6 +1093,9 @@ end = struct (* {{{ *)
   
   let perform_states query =
     if query = [] then [] else
+    let is_tac = function
+      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
+      | _ -> false in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1110,8 +1113,8 @@ end = struct (* {{{ *)
         if State.is_cached id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
-      | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n
-        when State.same_env o n -> (* A pure tactic *)
+      | Some (prev, o, `Cmd { cast = { expr }}), Some n
+        when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
           msg_warning (str "Sending back a fat state");
@@ -1638,6 +1641,7 @@ let collect_proof keep cur hd brkind id =
    | { expr = VernacPrint (PrintName _) } -> true
    | _ -> false in
  let parent = function Some (p, _) -> p | None -> assert false in
+ let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
@@ -1687,7 +1691,8 @@ let collect_proof keep cur hd brkind id =
      else if keep == VtDrop then `Sync (no_name,None,`Aborted)
      else
        let rc = collect (Some cur) [] id in
-       if (keep == VtKeep || keep == VtKeepAsAxiom) &&
+       if is_empty rc then make_sync `AlreadyEvaluated rc
+       else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
           (not(State.is_cached id) || !Flags.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
@@ -2124,9 +2129,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"VtProofMode must be executed VtNow")
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
-          VCS.checkout VCS.Branch.master;
           VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue});
-          VCS.propagate_sideff (Some x);
           List.iter
             (fun bn -> match VCS.get_branch bn with
             | { VCS.root; kind = `Master; pos } -> ()
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a0979f8b15..083fd54bfa 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -617,14 +617,17 @@ let rec tmpp v loc =
   | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
   | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
   | VernacNameSectionHypSet _ as x -> xmlTODO loc x
-  | VernacRequire (None,l) ->
-      xmlRequire loc (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some true,l) ->
-      xmlRequire loc ~attr:["export","true"] (List.map (fun ref ->
-        xmlReference ref) l)
-  | VernacRequire (Some false,l) ->
-      xmlRequire loc ~attr:["import","true"] (List.map (fun ref ->
+  | VernacRequire (from, import, l) ->
+      let import = match import with
+      | None -> []
+      | Some true -> ["export","true"]
+      | Some false -> ["import","true"]
+      in
+      let from = match from with
+      | None -> []
+      | Some r -> ["from", Libnames.string_of_reference r]
+      in
+      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (true,l) ->
       xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 4a3a287c08..cffbe48196 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -273,6 +273,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v
new file mode 100644
index 0000000000..fd394ddbc3
--- /dev/null
+++ b/test-suite/bugs/closed/3491.v
@@ -0,0 +1,4 @@
+(* Was failing while building the _rect scheme, due to wrong computation of *)
+(* the number of non recursively uniform parameters in the presence of let-ins*)
+Inductive list (A : Type) (T := A) : Type :=
+    nil : list A | cons : T -> list T -> list A.
diff --git a/test-suite/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v
new file mode 100644
index 0000000000..8e0a62d35c
--- /dev/null
+++ b/test-suite/bugs/closed/4165.v
@@ -0,0 +1,7 @@
+Lemma foo : True.
+Proof.
+pose (fun x : nat => (let H:=true in x)) as s.
+match eval cbv delta [s] in s with
+| context C[true] =>
+  let C':=context C[false] in pose C' as s'
+end.
diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v
deleted file mode 100644
index 9837b0ecb2..0000000000
--- a/test-suite/bugs/opened/3491.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail Inductive list (A : Type) (T := A) : Type :=
-    nil : list A | cons : T -> list T -> list A.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 3d4257543a..9661b3bfac 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -121,3 +121,44 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0.
 (* Check cross inference of evars from constructors *)
 
 Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
+
+(* An example with reduction removing an occurrence of the inductive type in one of its argument *)
+
+Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1).
+
+(* These types were considered as ill-formed before March 2015, while they
+   could be accepted considering that the type IND1 above was accepted *)
+
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
+
+Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A.
+
+Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A.
+
+(* This type was ok before March 2015 *)
+
+Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A.
+
+(* An example of nested positivity which was rejected by the kernel
+   before 24 March 2015 (even with Unset Elimination Schemes to avoid
+   the _rect bug) due to the wrong computation of non-recursively
+   uniform parameters in list' *)
+
+Inductive list' (A:Type) (B:=A) :=
+| nil' : list' A
+| cons' : A -> list' B -> list' A.
+
+Inductive tree := node : list' tree -> tree.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a bug in Inductiveops.get_arity in the presence of
+   let-ins and recursively non-uniform parameters. *)
+
+Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a wrong computation of the number of non-recursively
+   uniform parameters when conversion is needed, leading the example to
+   hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
+
+Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index cf9b8a087d..b5d0d22819 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -463,7 +463,7 @@ let variables is_install opt (args,defs) =
     print "ifeq ($(CAMLP4),camlp5)
 CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
 else
-CAMLP4EXTEND=
+CAMLP4EXTEND=threads.cma
 endif\n";
     print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
   $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
@@ -536,9 +536,13 @@ let include_dirs (inc_ml,inc_i,inc_r) =
       List.iter (fun x -> print "\\\n  "; print x) str_r; print "\n\n";
     end
 
+let double_colon = ["clean"; "cleanall"; "archclean"]
+
 let custom sps =
   let pr_path (file,dependencies,is_phony,com) =
-    print file; print ": "; print dependencies; print "\n";
+    print file;
+    print (if List.mem file double_colon then ":: " else ": ");
+    print dependencies; print "\n";
     if com <> "" then (print "\t"; print com; print "\n");
     print "\n"
   in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0b0fd4ef16..75e8369222 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1120,7 +1120,7 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  if Int.equal i 1 then begin
+  if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
     Notation.declare_notation_interpretation ntn scope pat df;
     (* Declare the uninterpretation *)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 6909d89440..4ee3bc4745 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -48,6 +48,10 @@ let print_usage_channel co command =
 \n  -compile f             compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
+\n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
+\n                         into fi.vo\
+\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
+\n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config                print Coq's configuration information and exit\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4ffae0fff..62e5f0a324 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -749,7 +749,11 @@ let vernac_end_segment (_,id as lid) =
 
 (* Libraries *)
 
-let vernac_require import qidl =
+let vernac_require from import qidl =
+  let qidl = match from with
+  | None -> qidl
+  | Some ns -> List.map (Libnames.join_reference ns) qidl
+  in
   let qidl = List.map qualid_of_reference qidl in
   let modrefl = List.map Library.try_locate_qualified_library qidl in
   if Dumpglob.dump () then
@@ -1884,7 +1888,7 @@ let interp ?proof locality poly c =
 
   | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
 
-  | VernacRequire (export, qidl) -> vernac_require export qidl
+  | VernacRequire (from, export, qidl) -> vernac_require from export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
   | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t