Restructuration of command.ml + generic infrastructure for inductive schemes

- Cleaning and uniformisation in command.ml:
  - For better modularity and better visibility, two files got isolated
    out of command.ml:
    - lemmas.ml is about starting and saving a proof
    - indschemes.ml is about declaring inductive schemes
  - Decomposition of the functions of command.ml into a functional part
    and the imperative part
- Inductive schemes:
  - New architecture in ind_tables.ml for registering scheme builders,
    and for sharing and generating on demand inductive schemes
  - Adding new automatically generated equality schemes (file eqschemes.ml)
    - "_congr" for equality types (completing here commit 12273)
    - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
      "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
      rewriting schemes (warning, rew_forward_dep cannot be stated following
      the standard Coq pattern for inductive types: "t=u" cannot be the
      last argument of the scheme)
    - "_case", "_case_nodep", "_case_dep" for case analysis schemes
  - Preliminary step towards discriminate and injection working on any
    equality-like type (e.g. eq_true)
  - Restating JMeq_congr under the canonical form of congruence schemes
  - Renamed "Set Equality Scheme" into "Set Equality Schemes"
  - Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
  - Activation of the automatic generation of boolean equality lemmas
  - Partial debug and error messages improvements for the generation of
    boolean equality and decidable equality
  - Added schemes for making dependent rewrite working (unfortunately with
    not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning

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

62 files changed, 2979 insertions, 1540 deletions

diff --git a/CHANGES b/CHANGES
index 152686e16..d76fe4bc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,8 +39,9 @@ Tactics
   is interpreted as using the collection of its constructors.
 - Tactic names "case" and "elim" now support clauses "as" and "in" and become
   then synonymous of "destruct" and "induction" respectively.
-- An new name "exfalso" for the use of 'ex-falso quodlibet' principle.
+- A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle.
   This tactic is simply a shortcut for "elimtype False".
+- Added support for Leibniz-rewriting of dependent hypotheses.
 
 Tactic Language
 
@@ -64,6 +65,11 @@ Vernacular commands
   "Reserved Notation".
 - Open/Close Scope command supports Global option in sections.
 - Ltac definitions support Local option for non-export outside modules.
+- Made generation of boolean equality automatic for datatypes (use
+  "Unset Boolean Equality Schemes" for deactivation).
+- Made support for automatic generation of case analysis schemes and
+  congruence schemes available to user (governed by options "Unset
+  Case Analysis Schemes" and "Unset Congruence Schemes").
 
 Tools
 
diff --git a/dev/base_include b/dev/base_include
index b6c2e4d08..41d1ac3bb 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -53,6 +53,7 @@
 open Names
 open Term
 open Typeops
+open Term_typing
 open Univ
 open Inductive
 open Indtypes
@@ -139,10 +140,14 @@ open Refine
 open Tacinterp
 open Tacticals
 open Tactics
+open Eqschemes
 
 open Cerrors
 open Class
 open Command
+open Indschemes
+open Ind_tables
+open Lemmas
 open Coqinit
 open Coqtop
 open Discharge
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ebbcb46ce..505141dd6 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,34 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Cleaning in commmand.ml
+
+Functions about starting/ending a lemma are in lemmas.ml
+Functions about inductive schemes are in indschemes.ml
+
+Functions renamed:
+
+declare_one_assumption -> declare_assumption
+declare_assumption -> declare_assumptions
+Command.syntax_definition -> Metasyntax.add_syntactic_definition
+declare_interning_data merged with add_notation_interpretation
+compute_interning_datas -> compute_full_internalization_env
+implicits_env -> internalization_env
+full_implicits_env -> full_internalization_env
+build_mutual -> do_mutual_inductive
+build_recursive -> do_fixpoint
+build_corecursive -> do_cofixpoint
+build_induction_scheme -> build_mutual_induction_scheme
+build_indrec -> build_induction_scheme
+instantiate_type_indrec_scheme -> weaken_sort_scheme
+instantiate_indrec_scheme -> modify_sort_scheme
+make_case_dep, make_case_nodep -> build_case_analysis_scheme
+make_case_gen -> build_case_analysis_scheme_default
+
+Types:
+
+decl_notation -> decl_notation option
+
 ** Cleaning in libnames/nametab interfaces
 
 Functions:
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4edf1a41d..4d5cdbb81 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4162,7 +4162,7 @@ general principle of mutual induction for objects in type {\term$_i$}.
 \SeeAlso Section~\ref{Scheme-examples}
 
 \subsection{Automatic declaration of schemes}
-\comindex{Set Equality Scheme}
+\comindex{Set Equality Schemes}
 \comindex{Set Elimination Schemes}
 It is possible to deactivate the automatic declaration of the induction
  principles when defining a new inductive type  with the
@@ -4171,7 +4171,7 @@ reactivated at any time with {\tt Set Elimination Schemes}.
 \\
 
 You can also activate the automatic declaration of those boolean equalities 
-(see the second variant of {\tt Scheme})  with the {\tt Set Equality Scheme}
+(see the second variant of {\tt Scheme})  with the {\tt Set Equality Schemes}
  command. However you have to be careful with this option since
 \Coq~ may now reject well-defined inductive types because it cannot compute
 a boolean equality for them.
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0057edad6..36a219a61 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -24,15 +24,32 @@ open Nametab
 open Notation
 open Inductiveops
 
-(* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions *)
-type var_internalisation_type = Inductive | Recursive | Method
-
-type var_internalisation_data =
-  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
-
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+(* To interpret implicits and arg scopes of variables in inductive
+   types and recursive definitions and of projection names in records *)
+
+type var_internalization_type = Inductive | Recursive | Method
+
+type var_internalization_data =
+    (* type of the "free" variable, for coqdoc, e.g. while typing the
+       constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+    var_internalization_type *
+    (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+       in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+    identifier list *
+    (* signature of impargs of the variable *)
+    Impargs.implicits_list *
+    (* subscopes of the args of the variable *)
+    scope_name option list
+
+type internalization_env =
+    (identifier * var_internalization_data) list
+
+type full_internalization_env =
+    (* a superset of the list of variables that may be automatically
+       inserted and that must not occur as binders *)
+    identifier list *
+    (* mapping of the variables to their internalization data *)
+    internalization_env
 
 type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
 
@@ -155,6 +172,35 @@ let error_inductive_parameter_not_implicit loc =
     "the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
 
 (**********************************************************************)
+(* Pre-computing the implicit arguments and arguments scopes needed   *)
+(* for interpretation *)
+
+let empty_internalization_env = ([],[])
+
+let set_internalization_env_params ienv params =
+  let nparams = List.length params in
+  if nparams = 0 then
+    ([],ienv)
+  else
+    let ienv_with_implicit_params =
+      List.map (fun (id,(ty,_,impl,scopes)) ->
+	let sub_impl,_ = list_chop nparams impl in
+	let sub_impl' = List.filter is_status_implicit sub_impl in
+	(id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in
+    (params, ienv_with_implicit_params)
+
+let compute_internalization_data env ty typ impls =
+  let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in
+  (ty, [], impl, compute_arguments_scope typ)
+
+let compute_full_internalization_env env ty params idl typl impll =
+  set_internalization_env_params
+    (list_map3
+      (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+      idl typl impll)
+    params
+
+(**********************************************************************)
 (* Contracting "{ _ }" in notations *)
 
 let rec wildcards ntn n =
@@ -368,7 +414,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 	(* [id] a goal variable *)
 	RVar (loc,id), [], [], []
 
-let find_appl_head_data (_,_,_,(_,impls)) = function
+let find_appl_head_data _ = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
@@ -1405,12 +1451,12 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_rawconstr c
 
-let interp_aconstr impls (vars,varslist) a =
+let interp_aconstr ?(impls=([],[])) (vars,varslist) a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
   let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
-    false (([],[]),Environ.named_context env,vl,([],impls)) a in
+    false (([],[]),Environ.named_context env,vl,impls) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b39f6e18b..b08b8dd1f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,19 +33,42 @@ open Pretyping
    - insert existential variables for implicit arguments
 *)
 
-(* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions; mention of a list of
-   implicits arguments in the ``rel'' part of [env]; the second
-   argument associates a list of implicit positions and scopes to
-   identifiers declared in the [rel_context] of [env] *)
+(* To interpret implicits and arg scopes of recursive variables while
+   internalizing inductive types and recursive definitions, and also
+   projection while typing records.
 
-type var_internalisation_type = Inductive | Recursive | Method
+   the third and fourth arguments associate a list of implicit
+   positions and scopes to identifiers declared in the [rel_context]
+   of [env] *)
 
-type var_internalisation_data =
-  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
+type var_internalization_type = Inductive | Recursive | Method
 
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+type var_internalization_data =
+    var_internalization_type *
+    identifier list *
+    Impargs.implicits_list *
+    scope_name option list
+
+(* A map of free variables to their implicit arguments and scopes *)
+type internalization_env =
+    (identifier * var_internalization_data) list
+
+(* Contains also a list of identifiers to automatically apply to the variables*)
+type full_internalization_env =
+    identifier list * internalization_env
+
+val empty_internalization_env : full_internalization_env
+
+val compute_internalization_data : env -> var_internalization_type ->
+  types -> Impargs.manual_explicitation list -> var_internalization_data
+
+val set_internalization_env_params :
+  internalization_env -> identifier list -> full_internalization_env
+
+val compute_full_internalization_env : env ->
+  var_internalization_type ->
+  identifier list -> identifier list -> types list ->
+  Impargs.manual_explicitation list list -> full_internalization_env
 
 type manual_implicits = (explicitation * (bool * bool * bool)) list
 
@@ -60,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 val intern_type : evar_map -> env -> constr_expr -> rawconstr
 
 val intern_gen : bool -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
 val intern_pattern : env -> cases_pattern_expr ->
@@ -69,12 +92,12 @@ val intern_pattern : env -> cases_pattern_expr ->
 
 val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
 
-(*s Composing internalisation with pretyping *)
+(*s Composing internalization with pretyping *)
 
 (* Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
 (* Particular instances *)
@@ -82,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env ->
   constr_expr -> constr
 
-val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
 val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
   constr_expr -> types -> constr
 
 (* Accepting evars and giving back the manual implicits in addition. *)
 
 val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env ->
-  ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+  ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
 
 val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_implicits_env ->
+  env -> ?impls:full_internalization_env ->
   constr_expr -> types * manual_implicits
 
 val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_implicits_env ->
+  env -> ?impls:full_internalization_env ->
   constr_expr -> constr * manual_implicits
 
 val interp_casted_constr_evars : evar_defs ref -> env ->
-  ?impls:full_implicits_env -> constr_expr -> types -> constr
+  ?impls:full_internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
+val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env ->
   constr_expr -> types
 
 (*s Build a judgment  *)
@@ -147,8 +170,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
 
-val interp_aconstr : implicits_env -> identifier list * identifier list
-  -> constr_expr -> interpretation
+val interp_aconstr : ?impls:full_internalization_env ->
+  identifier list * identifier list -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 90432a4a4..1ca82e35c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -215,9 +215,11 @@ type coq_eq_data = {
   trans: constr;
   congr: constr }
 
-type coq_rewrite_data = {
-  rrec : constr option;
-  rect : constr option
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+  inv_eq   : constr; (* : forall params, t -> Prop *)
+  inv_ind  : constr; (* : forall params P y, eq params y -> P y *)
+  inv_congr: constr  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
 }
 
 let lazy_init_constant dir id = lazy (init_constant dir id)
@@ -234,6 +236,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
 let coq_eq_sym  = lazy_init_constant ["Logic"] "eq_sym"
 let coq_eq_trans  = lazy_init_constant ["Logic"] "eq_trans"
 let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+  lazy_init_constant ["Logic"] "f_equal_canonical_form"
 
 let build_coq_eq_data () =
   let _ = check_required_library logic_module_name in {
@@ -245,11 +249,18 @@ let build_coq_eq_data () =
   congr = Lazy.force coq_eq_congr }
 
 let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
 let build_coq_f_equal2 () = Lazy.force coq_f_equal2
 
 let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
 
+let build_coq_inversion_eq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_eq;
+  inv_ind = Lazy.force coq_eq_ind;
+  inv_congr = Lazy.force coq_eq_congr_canonical }
+
 (* Heterogenous equality on Type *)
 
 let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
@@ -260,6 +271,8 @@ let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
 let coq_jmeq_sym  = lazy_logic_constant ["JMeq"] "JMeq_sym"
 let coq_jmeq_congr  = lazy_logic_constant ["JMeq"] "JMeq_congr"
 let coq_jmeq_trans  = lazy_logic_constant ["JMeq"] "JMeq_trans"
+let coq_jmeq_congr_canonical =
+  lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form"
 
 let build_coq_jmeq_data () =
   let _ = check_required_library jmeq_module_name in {
@@ -270,6 +283,17 @@ let build_coq_jmeq_data () =
   trans = Lazy.force coq_jmeq_trans;
   congr = Lazy.force coq_jmeq_congr }
 
+let join_jmeq_types eq =
+  mkLambda(Name (id_of_string "A"),Termops.new_Type(),
+  mkLambda(Name (id_of_string "x"),mkRel 1,
+  mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
+
+let build_coq_inversion_jmeq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq);
+  inv_ind = Lazy.force coq_jmeq_ind;
+  inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
 (* Specif *)
 let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
 
@@ -284,6 +308,7 @@ let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
 let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
 let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
 let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
+let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form"
 
 let build_coq_identity_data () =
   let _ = check_required_library datatypes_module_name in {
@@ -294,6 +319,25 @@ let build_coq_identity_data () =
   trans = Lazy.force coq_identity_trans;
   congr = Lazy.force coq_identity_congr }
 
+let build_coq_inversion_identity_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_type_module_name in {
+  inv_eq = Lazy.force coq_identity_eq;
+  inv_ind = Lazy.force coq_identity_ind;
+  inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_true_eq;
+  inv_ind = Lazy.force coq_eq_true_ind;
+  inv_congr = Lazy.force coq_eq_true_congr }
+
 (* The False proposition *)
 let coq_False  = lazy_init_constant ["Logic"] "False"
 
@@ -332,6 +376,7 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
 let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
 let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 8b0384960..6bb79c8b6 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -58,6 +58,9 @@ val check_required_library : string list -> unit
 val logic_module : dir_path
 val logic_type_module : dir_path
 
+val datatypes_module_name : string list
+val logic_module_name : string list
+
 (* Natural numbers *)
 val nat_path : full_path
 val glob_nat : global_reference
@@ -119,9 +122,22 @@ val build_coq_identity_data : coq_eq_data delayed
 val build_coq_jmeq_data : coq_eq_data delayed
 
 val build_coq_eq       : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl  : constr delayed (* = [(build_coq_eq_data()).refl] *)
 val build_coq_eq_sym   : constr delayed (* = [(build_coq_eq_data()).sym] *)
 val build_coq_f_equal2 : constr delayed
 
+(* Data needed for discriminate and injection *)
+
+type coq_inversion_data = {
+  inv_eq   : constr; (* : forall params, t -> Prop *)
+  inv_ind  : constr; (* : forall params P y, eq params y -> P y *)
+  inv_congr: constr  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
+
+val build_coq_inversion_eq_data : coq_inversion_data delayed
+val build_coq_inversion_identity_data : coq_inversion_data delayed
+val build_coq_inversion_jmeq_data : coq_inversion_data delayed
+val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
 (* Specif *)
 val build_coq_sumbool : constr delayed
@@ -154,6 +170,7 @@ val build_coq_ex : constr delayed
 val coq_eq_ref : global_reference lazy_t
 val coq_identity_ref : global_reference lazy_t
 val coq_jmeq_ref : global_reference lazy_t
+val coq_eq_true_ref : global_reference lazy_t
 val coq_existS_ref : global_reference lazy_t
 val coq_existT_ref : global_reference lazy_t
 val coq_not_ref : global_reference lazy_t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 04715d51b..df48458e6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -856,12 +856,17 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
-let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
 let mkCastC (a,k)  = CCast (dummy_loc,a,k)
 let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
 
+let mkAppC (f,l) =
+  let l = List.map (fun x -> (x,None)) l in
+  match f with
+  | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
+  | _ -> CApp (dummy_loc, (None, f), l)
+
 let rec mkCProdN loc bll c =
   match bll with
   | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
diff --git a/library/declare.ml b/library/declare.ml
index 1257044d3..ffe53e505 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -281,3 +281,37 @@ let declare_mind isrecord mie =
   !xml_declare_inductive (isrecord,oname);
   oname
 
+(* Declaration messages *)
+
+let pr_rank i = str (ordinal (i+1))
+
+let fixpoint_message indexes l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "no recursive definition"
+  | [id] -> pr_id id ++ str " is recursively defined" ++
+      (match indexes with
+	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+	 | _ -> mt ())
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+		  spc () ++ str "are recursively defined" ++
+		  match indexes with
+		    | Some a -> spc () ++ str "(decreasing respectively on " ++
+			prlist_with_sep pr_coma pr_rank (Array.to_list a) ++
+			str " arguments)"
+		    | None -> mt ()))
+
+let cofixpoint_message l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "No corecursive definition."
+  | [id] -> pr_id id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+                    spc () ++ str "are corecursively defined"))
+
+let recursive_message isfix i l =
+  (if isfix then fixpoint_message i else cofixpoint_message) l
+
+let definition_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is defined")
+
+let assumption_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is assumed")
diff --git a/library/declare.mli b/library/declare.mli
index 1a68f8e20..09526f341 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -59,10 +59,20 @@ val declare_internal_constant :
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : bool -> mutual_inductive_entry -> object_name
 
-(* hooks for XML output *)
+(* Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
 
-(* hook for the cache function of constants and inductives *)
+(* Hook for the cache function of constants and inductives *)
 val add_cache_hook : (full_path -> unit) -> unit
+
+(* Declaration messages *)
+
+val definition_message : identifier -> unit
+val assumption_message : identifier -> unit
+val fixpoint_message : int array option -> identifier list -> unit
+val cofixpoint_message : identifier list -> unit
+val recursive_message : bool (* true = fixpoint *) ->
+  int array option -> identifier list -> unit
+
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 949150ba5..3d789b92e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -968,7 +968,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	)
       ]
   in
-  Command.start_proof
+  Lemmas.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
@@ -977,7 +977,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     lemma_type
     (fun _ _ -> ());
   Pfedit.by (prove_replacement);
-  Command.save_named false
+  Lemmas.save_named false
 
 
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f6959d77e..ff4d1e972 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -303,7 +303,7 @@ let pp_dur time time' =
 (* let qed () = save_named true  *)
 let defined () =
   try
-    Command.save_named false
+    Lemmas.save_named false
   with
     | UserError("extract_proof",msg) ->
 	Util.errorlabstrm
@@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
-    Command.start_proof
+    Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
@@ -529,15 +529,14 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     List.map
       (fun (idx) ->
 	 let ind = first_fun_kn,idx in
-	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort
+	 ind,true,prop_sort
       )
       funs_indexes
   in
   let l_schemes =
     List.map
       (Typing.type_of env sigma)
-      (Indrec.build_mutual_indrec env sigma ind_list)
+      (Indrec.build_mutual_induction_scheme env sigma ind_list)
   in
   let i = ref (-1) in
   let sorts =
@@ -712,7 +711,7 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	 ind,prop_sort
   in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in
+  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun) in
   let sorts =
     (fun (_,_,x) ->
        Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 68850603b..77389681b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -150,7 +150,7 @@ let rec abstract_rawconstr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
 (*   Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
-  Constrintern.intern_gen false sigma env ~impls:([],impls)
+  Constrintern.intern_gen false sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 
@@ -166,15 +166,12 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
-        let arityc = Command.generalize_constr_expr arityc bl in
+        let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
-	let impl =
-	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits  env0 arity
-	  else [] in
-	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
-        (Environ.push_named (recname,None,arity) env, impls'))
+	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
+        (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls))
       (env0,[]) lnameargsardef in
+  let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
@@ -367,16 +364,15 @@ let generate_principle  on_error
 let register_struct is_rec fixpoint_exprl =
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+	let ce,imps =
+	  Command.interp_definition
+	    (Flags.boxed_definitions ()) bl None body (Some ret_type)
+	in
 	Command.declare_definition
-	  fname
-	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
-	  bl
-	  None
-  	  body
-	  (Some ret_type)
-	  (fun _ _ -> ())
+	  fname (Decl_kinds.Global,Decl_kinds.Definition)
+	  ce imps (fun _ _ -> ())
     | _ ->
-	Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
+	Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -389,7 +385,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Command.generalize_constr_expr ret_type args in
+  let type_of_f = Topconstr.prod_constr_expr ret_type args in
   let rec_arg_num =
     let names =
       List.map
@@ -420,7 +416,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Command.generalize_constr_expr unbounded_eq args in
+  let eq = Topconstr.prod_constr_expr unbounded_eq args in
   let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
       nb_args relation =
     try
@@ -531,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 			 raise (UserError("",str "Cannot find argument " ++
 					    Ppconstr.pr_id id))
 		     in
- 		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation)
+		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation option)
 		 | (name,None,args,types,body),recdef ->
 		     let names =  (Topconstr.names_of_local_assums args) in
 		     if  is_one_rec recdef  && List.length names > 1 then
@@ -541,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 		     else
 		       let loc, na = List.hd names in
 			 (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
-		     (None:Vernacexpr.decl_notation)
+		     (None:Vernacexpr.decl_notation option)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
 		     error
 		       ("Cannot use mutual definition with well-founded recursion or measure")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 116a3c991..ca93056ad 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -734,7 +734,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Command.save_named false
+let do_save () = Lemmas.save_named false
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
@@ -786,7 +786,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
@@ -823,10 +823,10 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let  mib,mip = Global.lookup_inductive graph_ind in
     let schemes =
       Array.of_list
-	(Indrec.build_mutual_indrec (Global.env ()) Evd.empty
+	(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i mip -> (kn,i),mib,mip,true,InType)
+		 (fun i _ -> (kn,i),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
@@ -838,7 +838,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 8aeff61e6..6dc36decf 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -904,7 +904,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
     } in *)
   let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
+  let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in
+  let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+  (* Declare the mutual inductive block with its associated schemes *)
+  ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
 
 
 (* Find infos on identifier id. *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 4bd0385ca..607734f22 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1364,7 +1364,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5499425df..d64b9728b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,8 +52,8 @@ open Genarg
 let compute_renamed_type gls c =
   rename_bound_var (pf_env gls) [] (pf_type_of gls c)
 
-let qed () = Command.save_named true
-let defined () = Command.save_named false
+let qed () = Lemmas.save_named true
+let defined () = Lemmas.save_named false
 
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
@@ -993,7 +993,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       )
       		 g)
 ;
-    Command.save_named opacity;
+    Lemmas.save_named opacity;
   in
   start_proof
     na
@@ -1042,7 +1042,7 @@ let com_terminate
     nb_args
     hook =
   let start_proof (tac_start:tactic) (tac_end:tactic) =
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     start_proof thm_name
       (Global, Proof Lemma) (Environ.named_context_val env)
       (hyp_terminates nb_args fonctional_ref) hook;
@@ -1322,7 +1322,7 @@ let (com_eqn : identifier ->
 	    else begin match cb.const_body with None -> true | _ -> false end
 	| _ -> anomaly "terminate_lemma: not a constant"
     in
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = (constr_of_global f_ref) in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
@@ -1343,7 +1343,7 @@ let (com_eqn : identifier ->
        );
 (*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () ->Command.save_named opacity) () ;
+     Flags.silently (fun () -> Lemmas.save_named opacity) () ;
 (*      Pp.msgnl (str "eqn finished"); *)
 
     );;
@@ -1358,7 +1358,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
 (*   Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
-  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in
+  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq in
 (*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index 07f32b6d4..019ffdbe7 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -787,9 +787,9 @@ let output_depends compute_depends ptree =
 
 let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' =
   Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[]));
-  Command.set_declare_assumption_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
-  Command.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
-  Command.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
+  Command.set_declare_assumptions_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
+  Lemmas.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
+  Lemmas.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
   Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt []))
 
 let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 85b55f36c..96bda6ecc 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -75,10 +75,10 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let evm, c, typ, imps =
-    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+    Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
-    Command.start_proof id kind c (fun loc gr ->
+    Lemmas.start_proof id kind c (fun loc gr ->
       Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
       hook loc gr)
 
@@ -93,14 +93,14 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_assumption env isevars idl is_coe k bl c nl =
+let declare_assumptions env isevars idl is_coe k bl c nl =
   if not (Pfedit.refining ()) then
     let id = snd (List.hd idl) in
     let evm, c, typ, imps =
-      Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
+      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
+      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -119,7 +119,7 @@ let vernac_assumption env isevars kind l nl =
 	List.iter (fun lid ->
 	  if global then Dumpglob.dump_definition lid (not global) "ax"
 	  else dump_variable lid) idl;
-      declare_assumption env isevars idl is_coe kind [] c nl) l
+      declare_assumptions env isevars idl is_coe kind [] c nl) l
 
 let check_fresh (loc,id) =
   if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index c47a1c4c4..26ac445c3 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -114,7 +114,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst =
-    let c = Command.generalize_constr_expr tclass ctx in
+    let c = Topconstr.prod_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
     let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 2a31d4e18..007013d40 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -294,13 +294,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
     let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
-    let impls = Command.compute_interning_datas env Constrintern.Recursive [] [recname] [full_arity] [impls] in
-    let newimpls =
-      match snd impls with
-      [(p, (r, l, impls, scopes))] ->
-	[(p, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))]
-      | x -> x
-    in interp_casted_constr isevars ~impls:(fst impls,newimpls)
+    let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in
+    let newimpls = [(recname, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))] in
+    let newimpls = Constrintern.set_internalization_env_params newimpls [] in
+    interp_casted_constr isevars ~impls:newimpls
       (push_rel_context ctx env) body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
@@ -412,7 +409,7 @@ let check_evars env initial_sigma evd c =
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
-  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
+  let kind = fixkind <> IsCoFixpoint in
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -433,13 +430,13 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in
+  let impls = Constrintern.compute_full_internalization_env env Constrintern.Recursive [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
     States.with_state_protection (fun () ->
-      List.iter (Command.declare_interning_data impls) notations;
+      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
 
@@ -478,7 +475,7 @@ let interp_recursive fixkind l boxed =
   in
   let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
     (match fixkind with
-      | Command.IsFixpoint wfl ->
+      | IsFixpoint wfl ->
 	  let possible_indexes =
 	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
 	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
@@ -487,7 +484,7 @@ let interp_recursive fixkind l boxed =
 	  in
 	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
 	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
-      | Command.IsCoFixpoint -> ());
+      | IsCoFixpoint -> ());
     Subtac_obligations.add_mutual_definitions defs notations fixkind
 
 let out_n = function
@@ -511,7 +508,7 @@ let build_recursive l b =
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
 	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
 	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l
-	  in interp_recursive (Command.IsFixpoint g) fixl b
+	  in interp_recursive (IsFixpoint g) fixl b
       | _, _ ->
 	  errorlabstrm "Subtac_command.build_recursive"
 	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
@@ -520,4 +517,4 @@ let build_corecursive l b =
   let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
     ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
     l in
-  interp_recursive Command.IsCoFixpoint fixl b
+  interp_recursive IsCoFixpoint fixl b
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 6c0c4340f..c9064ec82 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -13,7 +13,7 @@ val interp_gen :
   typing_constraint ->
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   ?allow_patvar:bool ->
   ?ltacvars:ltac_sign ->
   constr_expr -> constr
@@ -23,12 +23,12 @@ val interp_constr :
 val interp_type_evars :
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   constr_expr -> constr
 val interp_casted_constr_evars :
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   constr_expr -> types -> constr
 val interp_open_constr :
   evar_defs ref -> env -> constr_expr -> constr
@@ -54,7 +54,7 @@ val build_wellfounded :
            Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
 
 val build_recursive :
-  (fixpoint_expr * decl_notation) list -> bool -> unit
+  (fixpoint_expr * decl_notation option) list -> bool -> unit
 
 val build_corecursive :
-  (cofixpoint_expr * decl_notation) list -> bool -> unit
+  (cofixpoint_expr * decl_notation option) list -> bool -> unit
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 9b0b39cf8..45dfc44bc 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -45,6 +45,10 @@ type obligation =
 
 type obligations = (obligation array * int)
 
+type fixpoint_kind =
+  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsCoFixpoint
+
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type program_info = {
@@ -53,7 +57,7 @@ type program_info = {
   prg_type: constr;
   prg_obligations: obligations;
   prg_deps : identifier list;
-  prg_fixkind : Command.fixpoint_kind option ;
+  prg_fixkind : fixpoint_kind option ;
   prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
@@ -288,8 +292,8 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
-    List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
-    Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
+    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
+    Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
       first.prg_hook local gr;
@@ -435,7 +439,7 @@ let rec solve_obligation prg num =
       match deps_remaining obls obl.obl_deps with
       | [] ->
 	  let obl = subst_deps_obl obls obl in
-	    Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+	    Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
 	      (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 04e2371af..2666430a8 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -29,6 +29,10 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
+type fixpoint_kind =
+  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsCoFixpoint
+
 val add_mutual_definitions :
   (Names.identifier * Term.constr * Term.types *
       (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
@@ -36,7 +40,7 @@ val add_mutual_definitions :
   ?kind:Decl_kinds.definition_kind ->
   ?hook:Tacexpr.declaration_hook ->
   notations ->
-  Command.fixpoint_kind -> unit
+  fixpoint_kind -> unit
 
 val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
 
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 11a9fa9f5..e2910b8c4 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -110,12 +110,12 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id bl c tycon =
-  let c = Command.abstract_constr_expr c bl in
+  let c = Topconstr.abstract_constr_expr c bl in
   let tycon =
     match tycon with
 	None -> empty_tycon
       | Some t ->
-	  let t = Command.generalize_constr_expr t bl in
+	  let t = Topconstr.prod_constr_expr t bl in
 	  let t = coqintern_type !isevars env t in
 	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index fbe40525b..64f5fe9c7 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -323,7 +323,7 @@ let and_tac l hook =
 	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
   in
   let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
-    Command.start_proof and_proofid goal_kind and_goal
+    Lemmas.start_proof and_proofid goal_kind and_goal
       (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
     trace (str "Started and proof");
     Pfedit.by and_tac;
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f134614cb..e7dbc1af6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -8,6 +8,10 @@
 
 (* $Id$ *)
 
+(* File initially created by Christine Paulin, 1996 *)
+
+(* This file builds various inductive schemes *)
+
 open Pp
 open Util
 open Names
@@ -27,6 +31,8 @@ open Safe_typing
 open Nametab
 open Sign
 
+type dep_flag = bool
+
 (* Errors related to recursors building *)
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
@@ -43,16 +49,10 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (**********************************************************************)
 (* Building case analysis schemes *)
-(* Nouvelle version, plus concise mais plus coûteuse à cause de
-   lift_constructor et lift_inductive_family qui ne se contentent pas de
-   lifter les paramètres globaux *)
+(* Christine Paulin, 1996 *)
 
-let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
+let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   let lnamespar = mib.mind_params_ctxt in
-  let dep = match depopt with
-    | None -> inductive_sort_family mip <> InProp
-    | Some d -> d
-  in
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
@@ -108,6 +108,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
 
 (**********************************************************************)
 (* Building the recursive elimination *)
+(* Christine Paulin, 1996 *)
 
 (*
  * t is the type of the constructor co and recargs is the information on
@@ -428,7 +429,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
 	    lnamesparrec
       else
-	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind
+	mis_make_case_com dep env sigma indi (mibi,mipi) kind
   in
     (* Body of mis_make_indrec *)
     list_tabulate make_one_rec nrec
@@ -436,17 +437,18 @@ let mis_make_indrec env sigma listdepkind mib =
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
 
-let make_case_com depopt env sigma ity kind =
+let build_case_analysis_scheme env sigma ity dep kind =
   let (mib,mip) = lookup_mind_specif env ity in
-    mis_make_case_com depopt env sigma ity (mib,mip) kind
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
-let make_case_dep env   = make_case_com (Some true) env
-let make_case_nodep env = make_case_com (Some false) env
-let make_case_gen env   = make_case_com None env
+let build_case_analysis_scheme_default env sigma ity kind =
+  let (mib,mip) = lookup_mind_specif env ity in
+  let dep = inductive_sort_family mip <> InProp in
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
 
 (**********************************************************************)
-(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
+(* [modify_sort_scheme s rec] replaces the sort of the scheme
    [rec] by [s] *)
 
 let change_sort_arity sort =
@@ -460,7 +462,7 @@ let change_sort_arity sort =
     drec
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
-let instantiate_indrec_scheme sort =
+let modify_sort_scheme sort =
   let rec drec npar elim =
     match kind_of_term elim with
       | Lambda (n,t,c) ->
@@ -469,13 +471,13 @@ let instantiate_indrec_scheme sort =
 	  else
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "modify_sort_scheme: wrong elimination type"
   in
   drec
 
 (* Change the sort in the type of an inductive definition, builds the
    corresponding eta-expanded term *)
-let instantiate_type_indrec_scheme sort npars term =
+let weaken_sort_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
       | Prod (n,t,c) ->
@@ -488,7 +490,7 @@ let instantiate_type_indrec_scheme sort npars term =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
-      | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
   in
   drec npars
 
@@ -510,56 +512,29 @@ let check_arities listdepkind =
 	    [] listdepkind
   in true
 
-let build_mutual_indrec env sigma = function
-  | (mind,mib,mip,dep,s)::lrecspec ->
+let build_mutual_induction_scheme env sigma = function
+  | (mind,dep,s)::lrecspec ->
+      let (mib,mip) = Global.lookup_inductive mind in
       let (sp,tyi) = mind in
       let listdepkind =
-    	(mind,mib,mip, dep,s)::
+	(mind,mib,mip,dep,s)::
     	(List.map
-	   (function (mind',mibi',mipi',dep',s') ->
+	   (function (mind',dep',s') ->
 	      let (sp',_) = mind' in
 	      if sp=sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		(mind',mibi',mipi',dep',s')
 	      else
-		  raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+		raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
 	   lrecspec)
       in
       let _ = check_arities listdepkind in
       mis_make_indrec env sigma listdepkind mib
-  | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+  | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
 
-let build_indrec env sigma ind =
+let build_induction_scheme env sigma ind dep kind =
   let (mib,mip) = lookup_mind_specif env ind in
-  let kind = inductive_sort_family mip in
-  let dep = kind <> InProp in
-    List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
-
-(**********************************************************************)
-(* To handle old Case/Match syntax in Pretyping                       *)
-
-(*****************************************)
-(* To interpret Case and Match operators *)
-(* Expects a dependent predicate *)
-
-let type_rec_branches recursive env sigma indt p c =
-  let IndType (indf,realargs) = indt in
-  let (ind,params) = dest_ind_family indf in
-  let (mib,mip) = lookup_mind_specif env ind in
-  let recargs = mip.mind_recargs in
-  let tyi = snd ind in
-  let init_depPvec i = if i = tyi then Some(true,p) else None in
-  let depPvec = Array.init mib.mind_ntypes init_depPvec in
-  let constructors = get_constructors env indf in
-  let lft =
-    array_map2
-      (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
-      constructors (dest_subterms recargs) in
-  (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
-(* Non recursive case. Pb: does not deal with unification
-    let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
-    (p,ra)
-*)
+  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (*s Eliminations. *)
 
@@ -568,6 +543,8 @@ let elimination_suffix = function
   | InSet  -> "_rec"
   | InType -> "_rect"
 
+let case_suffix = "_case"
+
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 (* Look up function for the default elimination constant *)
@@ -595,59 +572,3 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
-
-(* Build the congruence lemma associated to an inductive type
-   I p1..pn a1..am with one constructor C : I q1..qn b1..bm *)
-
-(* TODO: extend it to types with more than one index *)
-
-let build_congr env (eq,refl) ind (mib,mip) =
-  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
-    error "Not an inductive type with a single constructor.";
-  if mip.mind_nrealargs <> 1 then
-    error "Expect an inductive type with one predicate parameter.";
-  let i = 1 in
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
-  if List.exists (fun (_,b,_) -> b <> None) realsign then
-    error "Inductive equalities with local definitions in arity not supported";
-  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
-  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
-  let _,constrargs = decompose_app ccl in
-  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
-    error "Constructor must have no arguments";
-  let c = List.nth constrargs (i + mib.mind_nparams - 1) in
-  let varB = id_of_string "B" in
-  let varH = id_of_string "H" in
-  let varf = id_of_string "f" in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
-  let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s in
-  let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name env c s in
-  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
-     (mkNamedLambda varB (new_Type ())
-     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
-     (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
-     (mkNamedLambda varH
-        (applist
-           (mkInd ind,
-	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
-	    extended_rel_list 0 realsign))
-     (mkCase (ci,
-       my_it_mkLambda_or_LetIn_name
-	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
-         (mkLambda
-           (Anonymous,
-            applist
-             (mkInd ind,
-	        extended_rel_list (2*mip.mind_nrealargs_ctxt+3)
-		  mib.mind_params_ctxt
-	        @ extended_rel_list 0 realsign),
-            mkApp (eq,
-	      [|mkVar varB;
-                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) c|]);
-		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
-       mkVar varH,
-       [|mkApp (refl,
-          [|mkVar varB;
-	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) c|])|])|]))))))
-
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index ac6a61c3c..91d559e17 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -27,36 +27,41 @@ exception RecursionSchemeError of recursion_scheme_error
 
 (** Eliminations *)
 
-(* These functions build elimination predicate for Case tactic *)
+type dep_flag = bool
 
-val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
+(* Build a case analysis elimination scheme in some sort family *)
 
-(* This builds an elimination scheme associated (using the own arity
-   of the inductive) *)
+val build_case_analysis_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val build_indrec : env -> evar_map -> inductive -> constr
-val instantiate_indrec_scheme : sorts -> int -> constr -> constr
-val instantiate_type_indrec_scheme : sorts -> int -> constr -> types ->
-  constr * types
+(* Build a dependent case elimination predicate unless type is in Prop *)
 
-(** Complex recursion schemes [Scheme] *)
+val build_case_analysis_scheme_default : env -> evar_map -> inductive ->
+      sorts_family -> constr
 
-val build_mutual_indrec :
-  env -> evar_map ->
-    (inductive * mutual_inductive_body * one_inductive_body
-    * bool * sorts_family) list
-    -> constr list
+(* Builds a recursive induction scheme (Peano-induction style) in the same
+   sort family as the inductive family; it is dependent if not in Prop *)
 
-(** Old Case/Match typing *)
+val build_induction_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val type_rec_branches : bool -> env -> evar_map -> inductive_type
-  -> constr -> constr -> constr array * constr
-val make_rec_branch_arg :
-  env -> evar_map ->
-    int * ('b * constr) option array * int ->
-    constr -> constructor_summary -> wf_paths list -> constr
+(* Builds mutual (recursive) induction schemes *)
+
+val build_mutual_induction_scheme :
+  env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list
+
+(** Scheme combinators *)
+
+(* [modify_sort_scheme s n c] modifies the quantification sort of
+   scheme c whose predicate is abstracted at position [n] of [c] *)
+
+val modify_sort_scheme : sorts -> int -> constr -> constr
+
+(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t]
+   whose conclusion is quantified on [Type] at position [n] of [t] a
+   scheme quantified on sort [s] *)
+
+val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types
 
 (** Recursor names utilities *)
 
@@ -64,5 +69,4 @@ val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier
 
-
-
+val case_suffix : string
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 11324ede9..e8ef6dd67 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -335,3 +335,22 @@ let reset_top_of_script () =
 	 up_until_matching_rule is_proof_instr pts
 	with Not_found -> top_of_tree pts)
 
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+open Decl_kinds
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let build_by_tactic typ tac =
+  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Decls.clear_proofs (Global.named_context ()) in
+  start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
+  try
+    by tac;
+    let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
+    delete_current_proof ();
+    const.const_entry_body
+  with e ->
+    delete_current_proof ();
+    raise e
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8dcd8edc2..f46825b0c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,5 +190,11 @@ val traverse_prev_unproven : unit -> unit
 
 (* These two functions make it possible to implement more elaborate
    proof and goal management, as it is done, for instance in pcoq *)
+
 val traverse_to : int list -> unit
 val mutate : (pftreestate -> pftreestate) -> unit
+
+
+(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+
+val build_by_tactic : types -> tactic -> constr
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
new file mode 100644
index 000000000..058abb2b7
--- /dev/null
+++ b/tactics/eqschemes.ml
@@ -0,0 +1,619 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* File created by Hugo Herbelin, Nov 2009 *)
+
+(* This file builds schemes related to equality inductive types,
+   especially for dependent rewrite, rewriting on arbitrary equality
+   types and congruence on arbitrary equality types *)
+
+(* However, the choices made lack uniformity, as we have to make a
+   compromise between several constraints and ideal requirements:
+
+   - Having the extended schemes working conservatively over the
+     existing non-dependent schemes eq_rect and eq_rect_r. There is in
+     particular a problem with the dependent rewriting schemes in
+     hypotheses for which the inductive types cannot be in last
+     position of the scheme as it is the general rule in Coq. This has
+     an effect on the order of generated goals (side-conditions of the
+     lemma after or before the main goal). The non-dependent case can be
+     fixed but to the price of a lost of uniformity wrt side-conditions
+     in the dependent and non-dependent cases.
+
+   - Having schemes general enough to support non-symmetric equality
+     type like eq_true.
+
+   - Having schemes that avoid introducing beta-expansions blocked by
+     "match" so as to please the guard condition, but this introduces
+     some tricky things involving involutivity of symmetry that I
+     don't how to avoid. The result below is a compromise with
+     dependent left-to-right rewriting in conclusion (l2r_dep) using
+     the tricky involutivity of symmetry and dependent left-to-right
+     rewriting in hypotheses (l2r_forward_dep), that one wants to be
+     used for non-symmetric equality and that introduces blocked
+     beta-expansions.
+
+   One may wonder whether these extensions are worth to be done
+   regarding the price we have to pay and regarding the rare
+   situations where they are needed. However, I believe it meets a 
+   natural expectation of the user.
+*)
+
+open Util
+open Names
+open Term
+open Declarations
+open Environ
+open Inductive
+open Termops
+open Inductiveops
+open Ind_tables
+open Indrec
+
+let hid = id_of_string "H"
+let xid = id_of_string "X"
+let default_id_of_sort = function InProp _ | InSet -> hid | InType _ -> xid
+let fresh env id = next_global_ident_away false id []
+
+let build_dependent_inductive ind (mib,mip) =
+  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  applist
+    (mkInd ind,
+       extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
+       @ extended_rel_list 0 realargs)
+
+let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s
+let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn ~init:c s
+let my_it_mkLambda_or_LetIn_name s c =
+  it_mkLambda_or_LetIn_name (Global.env()) c s
+
+let get_coq_eq () =
+  try
+    let eq = Libnames.destIndRef Coqlib.glob_eq in
+    let _ = Global.lookup_inductive eq in
+    (* Do not force the lazy if they are not defined *)
+    mkInd eq, Coqlib.build_coq_eq_refl ()
+  with Not_found ->
+    error "eq not found."
+
+let get_sym_eq_data env ind =
+  let (mib,mip as specif) = lookup_mind_specif env ind in
+  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+    error "Not an inductive type with a single constructor.";
+  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  if List.exists (fun (_,b,_) -> b <> None) realsign then
+    error "Inductive equalities with local definitions in arity not supported.";
+  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let _,constrargs = decompose_app ccl in
+  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+    error "Constructor must have no arguments"; (* This can be relaxed... *)
+  let params,constrargs = list_chop mib.mind_nparams constrargs in
+  if mip.mind_nrealargs > mib.mind_nparams then
+    error "Constructors arguments must repeat the parameters.";
+  let _,params2 = list_chop (mib.mind_nparams-mip.mind_nrealargs) params in
+  let paramsctxt1,_ =
+    list_chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
+  if params2 <> constrargs then
+    error "Constructors arguments must repeat the parameters.";
+  (* nrealargs_ctxt and nrealargs are the same here *)
+  (specif,mip.mind_nrealargs,realsign,mib.mind_params_ctxt,paramsctxt1)
+
+let get_non_sym_eq_data env ind =
+  let (mib,mip as specif) = lookup_mind_specif env ind in
+  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+    error "Not an inductive type with a single constructor.";
+  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  if List.exists (fun (_,b,_) -> b <> None) realsign then
+    error "Inductive equalities with local definitions in arity not supported";
+  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let _,constrargs = decompose_app ccl in
+  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+    error "Constructor must have no arguments";
+  let _,constrargs = list_chop mib.mind_nparams constrargs in
+  (specif,constrargs,realsign,mip.mind_nrealargs)
+
+(**********************************************************************)
+(* Build the symmetry lemma associated to an inductive type           *)
+(* I q1..qm,p1..pn a1..an with one constructor                        *)
+(* C : I q1..qm,p1..pn p1..pn                                         *)
+(*                                                                    *)
+(* sym := fun q1..qn p1..pn a1..an (H:I q1..qm p1..pn a1..an) =>      *)
+(*        match H in I _.._ a1..an return I q1..qm a1..an p1..pn with *)
+(*            C => C                                                  *)
+(*        end                                                         *)
+(*      : forall q1..qm p1..pn a1..an I q1..qm p1..pn a1..an ->       *)
+(*          I q1..qm a1..an p1..pn                                    *)
+(*                                                                    *)
+(**********************************************************************)
+
+let build_sym_scheme env ind =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+    get_sym_eq_data env ind in
+  let cstr n =
+    mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in
+  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let applied_ind = build_dependent_inductive ind specif in
+  let realsign_ind =
+    name_context env ((Name varH,None,applied_ind)::realsign) in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+  (my_it_mkLambda_or_LetIn_name realsign_ind
+  (mkCase (ci,
+     my_it_mkLambda_or_LetIn_name
+       (lift_rel_context (nrealargs+1) realsign_ind)
+       (mkApp (mkInd ind,Array.concat
+	  [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	   rel_vect 1 nrealargs;
+	   rel_vect (2*nrealargs+2) nrealargs])),
+     mkRel 1 (* varH *),
+       [|cstr (nrealargs+1)|]))))
+
+let sym_scheme_kind =
+  declare_individual_scheme_object "_sym"
+  (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind)
+
+(**********************************************************************)
+(* Build the involutivity of symmetry for an inductive type           *)
+(* I q1..qm,p1..pn a1..an with one constructor                        *)
+(* C : I q1..qm,p1..pn p1..pn                                         *)
+(*                                                                    *)
+(* inv := fun q1..qn p1..pn a1..an (H:I q1..qm p1..pn a1..an) =>      *)
+(*        match H in I _.._ a1..an return                             *)
+(*          sym q1..qm p1..pn a1..an (sym q1..qm a1..an p1..pn H) = H *)
+(*        with                                                        *)
+(*          C => refl_equal C                                         *)
+(*        end                                                         *)
+(*      : forall q1..qm p1..pn a1..an (H:I q1..qm a1..an p1..pn),     *)
+(*          sym q1..qm p1..pn a1..an (sym q1..qm a1..an p1..pn H) = H *)
+(*                                                                    *)
+(**********************************************************************)
+
+let build_sym_involutive_scheme env ind =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+    get_sym_eq_data env ind in
+  let sym = mkConst (find_scheme sym_scheme_kind ind) in
+  let (eq,eqrefl) = get_coq_eq () in
+  let cstr n = mkApp (mkConstruct(ind,1),extended_rel_vect n paramsctxt) in
+  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let applied_ind = build_dependent_inductive ind specif in
+  let applied_ind_C =
+    mkApp
+      (mkInd ind, Array.append
+         (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
+         (rel_vect (nrealargs+1) nrealargs)) in
+  let realsign_ind =
+    name_context env ((Name varH,None,applied_ind)::realsign) in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  (my_it_mkLambda_or_LetIn paramsctxt
+  (my_it_mkLambda_or_LetIn_name realsign_ind
+  (mkCase (ci,
+     my_it_mkLambda_or_LetIn_name
+       (lift_rel_context (nrealargs+1) realsign_ind)
+       (mkApp (eq,[|
+	 mkApp
+	   (mkInd ind, Array.concat
+	     [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	      rel_vect (2*nrealargs+2) nrealargs;
+	      rel_vect 1 nrealargs]);
+         mkApp (sym,Array.concat
+	   [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+            rel_vect 1 nrealargs;
+            rel_vect (2*nrealargs+2) nrealargs;
+            [|mkApp (sym,Array.concat
+	      [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       rel_vect (2*nrealargs+2) nrealargs;
+	       rel_vect 1 nrealargs;
+	       [|mkRel 1|]])|]]);
+	 mkRel 1|])),
+     mkRel 1 (* varH *),
+       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+
+let sym_involutive_scheme_kind =
+  declare_individual_scheme_object "_sym_involutive"
+  (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
+
+(**********************************************************************)
+(* Build the left-to-right rewriting lemma for conclusion associated  *)
+(* to an inductive type I q1..qm,p1..pn a1..an with one constructor   *)
+(* C : I q1..qm,p1..pn p1..pn                                         *)
+(* (symmetric equality in non-dependent and dependent cases)          *)
+(*                                                                    *)
+(* We could have defined the scheme in one match over a generalized   *)
+(* type but this behaves badly wrt the guard condition, so we use     *)
+(* symmetry instead                                                   *)
+(*                                                                    *)
+(* ind_rd := fun q1..qm p1..pn a1..an                                 *)
+(*               (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind)    *)
+(*               (HC:P a1..an C)                                      *)
+(*               (H:I q1..qm p1..pn a1..an)  =>                       *)
+(*           match sym_involutive q1..qm p1..pn a1..an H as Heq       *)
+(*               in _ = H return P p1..pn H                           *)
+(*           with                                                     *)
+(*             refl =>                                                *)
+(*               match sym q1..qm p1..pn a1..an H as H                *)
+(*                      in I _.._ p1..pn                              *)
+(*                     return P p1..pn (sym q1..qm a1..an p1..pn H)   *)
+(*               with                                                 *)
+(*                 C => HC                                            *)
+(*               end                                                  *)
+(*           end                                                      *)
+(*       : forall q1..qn p1..pn a1..an                                *)
+(*           (P:forall p1..pn, I q1..qm p1..pn a1..an ->kind),        *)
+(*           P a1..an C ->                                            *)
+(*           forall (H:I q1..qm p1..pn a1..an), P p1..pn H            *)
+(*                                                                    *)
+(* where A1..An are the common types of p1..pn and a1..an             *)
+(**********************************************************************)
+
+let build_l2r_rew_scheme dep env ind kind =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+    get_sym_eq_data env ind in
+  let sym = mkConst (find_scheme sym_scheme_kind ind) in
+  let sym_involutive = mkConst (find_scheme sym_involutive_scheme_kind ind) in
+  let (eq,eqrefl) = get_coq_eq () in
+  let cstr n p =
+    mkApp (mkConstruct(ind,1),
+      Array.concat [extended_rel_vect n paramsctxt1;
+                    rel_vect p nrealargs]) in
+  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let varHC = fresh env (id_of_string "HC") in
+  let varP = fresh env (id_of_string "P") in
+  let applied_ind = build_dependent_inductive ind specif in
+  let applied_ind_P =
+    mkApp (mkInd ind, Array.concat
+       [extended_rel_vect (3*nrealargs) paramsctxt1;
+        rel_vect 0 nrealargs;
+        rel_vect nrealargs nrealargs]) in
+  let applied_ind_G =
+    mkApp (mkInd ind, Array.concat
+       [extended_rel_vect (3*nrealargs+3) paramsctxt1;
+        rel_vect (nrealargs+3) nrealargs;
+        rel_vect 0 nrealargs]) in
+  let realsign_P = lift_rel_context nrealargs realsign in
+  let realsign_ind_P =
+    name_context env ((Name varH,None,applied_ind_P)::realsign_P) in
+  let realsign_ind_G =
+    name_context env ((Name varH,None,applied_ind_G)::
+                      lift_rel_context (nrealargs+3) realsign) in
+  let applied_sym_C n =
+     mkApp(sym,
+       Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+  let applied_sym_G =
+     mkApp(sym,
+       Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1;
+                     rel_vect (nrealargs+4) nrealargs;
+                     rel_vect 1 nrealargs;
+		     [|mkRel 1|]]) in
+  let s = mkSort (new_sort_in_family kind) in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let cieq = make_case_info (Global.env()) (destInd eq) RegularStyle in
+  let applied_PC =
+    mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
+           (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
+  let applied_PG =
+    mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
+           (if dep then [|applied_sym_G|] else [||])) in
+  let applied_PR =
+    mkApp (mkVar varP,Array.append (rel_vect (nrealargs+5) nrealargs)
+           (if dep then [|mkRel 2|] else [||])) in
+  let applied_sym_sym =
+         mkApp (sym,Array.concat
+	   [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+            rel_vect 4 nrealargs;
+            rel_vect (nrealargs+4) nrealargs;
+            [|mkApp (sym,Array.concat
+	      [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	       rel_vect (nrealargs+4) nrealargs;
+	       rel_vect 4 nrealargs;
+	       [|mkRel 2|]])|]]) in
+  (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+  (my_it_mkLambda_or_LetIn_name realsign
+  (mkNamedLambda varP
+    (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s)
+  (mkNamedLambda varHC applied_PC
+  (mkNamedLambda varH (lift 2 applied_ind)
+  (mkCase (cieq,
+     mkLambda (Name varH,lift 3 applied_ind,
+       mkLambda (Anonymous,
+                 mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
+                 applied_PR)),
+     (mkApp (sym_involutive,
+       Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|])),
+     [|mkCase (ci,
+        my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
+        applied_sym_C 3,
+        [|mkVar varHC|])|])))))))
+
+
+(**********************************************************************)
+(* Build the right-to-left rewriting lemma for hypotheses associated  *)
+(* to an inductive type I q1..qm,p1..pn a1..an with one constructor   *)
+(* C : I q1..qm,p1..pn p1..pn                                         *)
+(* (symmetric equality in dependent cases)                            *)
+(*                                                                    *)
+(* rew := fun q1..qm p1..pn a1..an (H:I q1..qm p1..pn a1..an)         *)
+(*          match H in I _.._ a1..an                                  *)
+(*                 return forall                                      *)
+(*                  (P:forall p1..pn, I q1..qm p1..pn a1..an -> kind) *)
+(*                  (HC:P p1..pn H) =>                                *)
+(*                  P a1..an C                                        *)
+(*          with                                                      *)
+(*             C => fun P HC => HC                                    *)
+(*          end                                                       *)
+(*       : forall q1..qm p1..pn a1..an                                *)
+(*           (H:I q1..qm p1..pn a1..an)                               *)
+(*           (P:forall p1..pn, I q1..qm p1..pn a1..an ->kind),        *)
+(*           P p1..pn H -> P a1..an C                                 *)
+(*                                                                    *)
+(**********************************************************************)
+
+let build_r2l_forward_rew_scheme dep env ind kind =
+  let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
+    get_sym_eq_data env ind in
+  let cstr n p =
+    mkApp (mkConstruct(ind,1),
+      Array.concat [extended_rel_vect n paramsctxt1;
+                    rel_vect p nrealargs]) in
+  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let varHC = fresh env (id_of_string "HC") in
+  let varP = fresh env (id_of_string "P") in
+  let applied_ind = build_dependent_inductive ind specif in
+  let applied_ind_P =
+    mkApp (mkInd ind, Array.concat
+       [extended_rel_vect (4*nrealargs+2) paramsctxt1;
+        rel_vect 0 nrealargs;
+        rel_vect (nrealargs+1) nrealargs]) in
+  let applied_ind_P' =
+    mkApp (mkInd ind, Array.concat
+       [extended_rel_vect (3*nrealargs+1) paramsctxt1;
+        rel_vect 0 nrealargs;
+        rel_vect (2*nrealargs+1) nrealargs]) in
+  let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
+  let realsign_ind =
+    name_context env ((Name varH,None,applied_ind)::realsign) in
+  let realsign_ind_P n aP =
+    name_context env ((Name varH,None,aP)::realsign_P n) in
+  let s = mkSort (new_sort_in_family kind) in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let applied_PC =
+    mkApp (mkVar varP,Array.append
+           (rel_vect (nrealargs*2+3) nrealargs)
+           (if dep then [|mkRel 2|] else [||])) in
+  let applied_PC' =
+    mkApp (mkVar varP,Array.append
+           (rel_vect (nrealargs+2) nrealargs)
+           (if dep then [|cstr (2*nrealargs+2) (nrealargs+2)|]
+	    else [||])) in
+  let applied_PG =
+    mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs)
+           (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in
+  (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+  (my_it_mkLambda_or_LetIn_name realsign
+  (mkNamedLambda varH applied_ind
+  (mkCase (ci,
+     my_it_mkLambda_or_LetIn_name
+       (lift_rel_context (nrealargs+1) realsign_ind)
+       (mkNamedProd varP
+         (my_it_mkProd_or_LetIn
+	   (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
+       (mkNamedProd varHC applied_PC applied_PG)),
+     (mkVar varH),
+     [|mkNamedLambda varP
+        (my_it_mkProd_or_LetIn
+	  (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
+      (mkNamedLambda varHC applied_PC'
+	(mkVar varHC))|])))))
+
+(**********************************************************************)
+(* Build the left-to-right rewriting lemma for hypotheses associated  *)
+(* to an inductive type I q1..qm a1..an with one constructor          *)
+(* C : I q1..qm b1..bn  (dependent case)                              *)
+(*                                                                    *)
+(* ind_rd := fun q1..qm a1..an (H:I q1..qm a1..an)                    *)
+(*             (P:forall a1..an, I q1..qm a1..an -> kind)             *)
+(*             (HC:P a1..an H) =>                                     *)
+(*           match H in I _.._ a1..an return P a1..an H -> P b1..bn C *)
+(*           with                                                     *)
+(*             C => fun x => x                                        *)
+(*           end HC                                                   *)
+(*      : forall q1..pm a1..an (H:I q1..qm a1..an)                    *)
+(*               (P:forall a1..an, I q1..qm a1..an -> kind),          *)
+(*               P a1..an H -> P b1..bn C                             *)
+(*                                                                    *)
+(* Note that the dependent elimination in ind_rd is not a dependency  *)
+(* in the conclusion of the scheme but a dependency in the premise of *)
+(* the scheme. This is unfortunately incompatible with the standard   *)
+(* pattern for schemes in Coq which expects that the eliminated       *)
+(* object is the last premise of the scheme. We then have no choice   *)
+(* than following the more liberal pattern of having the eliminated   *)
+(* object coming before the premises.                                 *)
+(**********************************************************************)
+
+let build_l2r_forward_rew_scheme dep env ind kind =
+  let ((mib,mip as specif),constrargs,realsign,nrealargs) =
+    get_non_sym_eq_data env ind in
+  let cstr n =
+    mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in
+  let constrargs_cstr = constrargs@[cstr 0] in
+  let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
+  let varHC = fresh env (id_of_string "HC") in
+  let varP = fresh env (id_of_string "P") in
+  let applied_ind = build_dependent_inductive ind specif in
+  let realsign_ind =
+    name_context env ((Name varH,None,applied_ind)::realsign) in
+  let s = mkSort (new_sort_in_family kind) in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let applied_PC =
+    applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
+  let applied_PG =
+    mkApp (mkVar varP,
+           if dep then extended_rel_vect 0 realsign_ind
+	   else extended_rel_vect 1 realsign) in
+  (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+  (my_it_mkLambda_or_LetIn_name realsign_ind
+  (mkNamedLambda varP
+    (my_it_mkProd_or_LetIn (lift_rel_context (nrealargs+1)
+                             (if dep then realsign_ind else realsign)) s)
+  (mkNamedLambda varHC (lift 1 applied_PG)
+  (mkApp
+    (mkCase (ci,
+       my_it_mkLambda_or_LetIn_name
+         (lift_rel_context (nrealargs+3) realsign_ind)
+         (mkArrow applied_PG (lift (2*nrealargs+5) applied_PC)),
+       mkRel 3 (* varH *),
+       [|mkLambda
+          (Name varHC,
+	   lift (nrealargs+3) applied_PC,
+	   mkRel 1)|]),
+    [|mkVar varHC|]))))))
+
+(**********************************************************************)
+(* This function "repairs" the non-dependent l2r forward rewriting    *)
+(* scheme by making it comply with the standard pattern of schemes    *)
+(* in Coq. Otherwise said, it turns a scheme of type                  *)
+(*                                                                    *)
+(*  forall q1..pm a1..an (H:I q1..qm a1..an)                          *)
+(*         (P:forall a1..an, I q1..qm a1..an -> kind),                *)
+(*         P a1..an H -> P b1..bn C                                   *)
+(*                                                                    *)
+(* into a scheme of type                                              *)
+(*                                                                    *)
+(*  forall q1..pm a1..an (P:forall a1..an, I q1..qm a1..an -> kind),  *)
+(*         P a1..an H -> forall (H:I q1..qm a1..an), P b1..bn C       *)
+(*                                                                    *)
+(**********************************************************************)
+
+let fix_l2r_forward_rew_scheme c =
+  let t = Retyping.get_type_of (Global.env()) Evd.empty c in
+  let ctx,_ = decompose_prod_assum t in
+  match ctx with
+  | hp :: p :: ind :: indargs ->
+      my_it_mkLambda_or_LetIn indargs
+	(mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind)
+	      (Reductionops.whd_beta Evd.empty
+		(applist (c,
+	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+  | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme"
+
+(**********************************************************************)
+
+let build_r2l_rew_scheme dep env ind k =
+  build_case_analysis_scheme env Evd.empty ind dep k
+
+(* Dependent rewrite from left-to-right in conclusion *)
+let rew_l2r_dep_scheme_kind =
+  declare_individual_scheme_object "_rew_r_dep"
+  (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+
+(* Dependent rewrite from left-to-right in hypotheses *)
+let rew_l2r_forward_dep_scheme_kind =
+  declare_individual_scheme_object "_rew_fwd_dep"
+  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
+
+(* Dependent rewrite from right-to-left in conclusion *)
+let rew_r2l_dep_scheme_kind =
+  declare_individual_scheme_object "_rew_dep"
+  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
+
+(* Dependent rewrite from right-to-left in hypotheses *)
+let rew_r2l_forward_dep_scheme_kind =
+  declare_individual_scheme_object "_rew_fwd_r_dep"
+  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
+
+(* Rewrite from left-to-right in conclusion and left-to-right in hypotheses *)
+let rew_l2r_scheme_kind =
+  declare_individual_scheme_object "_rew_r"
+  (fun ind ->
+    (* For the non-dependent case, we have two possible choices: *)
+    (* - build_l2r_forward_rew_scheme is ok even for non symmetric *)
+    (*   equality like eq_true but it introduced a beta-expansion blocked *)
+    (*   by the match and thus, it makes the guard condition fragile *)
+    (*   Moreover, its standard form needs the inductive hypothesis not *)
+    (*   in last position what breaks the order of goals and need a fix! *)
+    (* - build_l2r_rew_scheme uses symmetry and is better for guard *)
+    (*   but it does not work for non-symmetric equalities *)
+    fix_l2r_forward_rew_scheme
+      (build_l2r_forward_rew_scheme false (Global.env()) ind InType))
+
+(* Rewrite from right-to-left in conclusion and left-to-right in hypotheses *)
+let rew_r2l_scheme_kind =
+  declare_individual_scheme_object "_rew"
+  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
+
+(**********************************************************************)
+(* Build the congruence lemma associated to an inductive type         *)
+(* I p1..pn a with one constructor C : I q1..qn b                     *)
+(*                                                                    *)
+(* congr := fun p1..pn (B:Type) (f:A->B) a (H:I p1..pn a) =>          *)
+(*          match H in I _.._ a' return f b = f a' with               *)
+(*            C => eq_refl (f b)                                      *)
+(*          end                                                       *)
+(*       : forall p1..pn (B:Type) (f:A->B) a, I p1..pn a -> f b = f a *)
+(*                                                                    *)
+(* where A is the common type of a and b                              *)
+(**********************************************************************)
+
+(* TODO: extend it to types with more than one index *)
+
+let build_congr env (eq,refl) ind =
+  let (mib,mip) = lookup_mind_specif env ind in
+  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+    error "Not an inductive type with a single constructor.";
+  if mip.mind_nrealargs <> 1 then
+    error "Expect an inductive type with one predicate parameter.";
+  let i = 1 in
+  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  if List.exists (fun (_,b,_) -> b <> None) realsign then
+    error "Inductive equalities with local definitions in arity not supported.";
+  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
+  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let _,constrargs = decompose_app ccl in
+  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+    error "Constructor must have no arguments";
+  let b = List.nth constrargs (i + mib.mind_nparams - 1) in
+  let varB = fresh env (id_of_string "B") in
+  let varH = fresh env (id_of_string "H") in
+  let varf = fresh env (id_of_string "f") in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+     (mkNamedLambda varB (new_Type ())
+     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
+     (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
+     (mkNamedLambda varH
+        (applist
+           (mkInd ind,
+	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
+	    extended_rel_list 0 realsign))
+     (mkCase (ci,
+       my_it_mkLambda_or_LetIn_name
+	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
+         (mkLambda
+           (Anonymous,
+            applist
+             (mkInd ind,
+	        extended_rel_list (2*mip.mind_nrealargs_ctxt+3)
+		  mib.mind_params_ctxt
+	        @ extended_rel_list 0 realsign),
+            mkApp (eq,
+	      [|mkVar varB;
+                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) b|]);
+		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+       mkVar varH,
+       [|mkApp (refl,
+          [|mkVar varB;
+	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+
+let congr_scheme_kind = declare_individual_scheme_object "_congr"
+  (fun ind ->
+    (* May fail if equality is not defined *)
+    build_congr (Global.env()) (get_coq_eq ()) ind)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
new file mode 100644
index 000000000..bf72245d6
--- /dev/null
+++ b/tactics/eqschemes.mli
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(* This file builds schemes relative to equality inductive types *)
+
+open Names
+open Term
+open Environ
+open Ind_tables
+
+(* Builds a left-to-right rewriting scheme for an equality type *)
+
+val rew_l2r_dep_scheme_kind : individual scheme_kind
+val rew_l2r_scheme_kind : individual scheme_kind
+val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
+val rew_r2l_forward_dep_scheme_kind : individual scheme_kind
+val rew_r2l_dep_scheme_kind : individual scheme_kind
+val rew_r2l_scheme_kind : individual scheme_kind
+
+val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_forward_rew_scheme :
+  bool -> env -> inductive -> sorts_family -> constr
+val build_r2l_forward_rew_scheme :
+  bool -> env -> inductive -> sorts_family -> constr
+
+(* Builds a symmetry scheme for a symmetrical equality type *)
+
+val build_sym_scheme : env -> inductive -> constr
+val sym_scheme_kind : individual scheme_kind
+
+val build_sym_involutive_scheme : env -> inductive -> constr
+val sym_involutive_scheme_kind : individual scheme_kind
+
+(* Builds a congruence scheme for an equality type *)
+
+val congr_scheme_kind : individual scheme_kind
+val build_congr : env -> constr * constr -> inductive -> constr
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9957e8a39..8ad73c672 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -43,6 +43,8 @@ open Printer
 open Clenv
 open Clenvtac
 open Evd
+open Ind_tables
+open Eqschemes
 
 (* Options *)
 
@@ -173,28 +175,45 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
-let find_elim hdcncl lft2rgt cls gl =
-  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-  let hdcncls = string_of_inductive hdcncl ^ suffix in
-  let rwr_thm = if lft2rgt = (cls = None) then hdcncls^"_r" else hdcncls in
-  try pf_global gl (id_of_string rwr_thm)
-  with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
+let find_elim hdcncl lft2rgt dep cls =
+  let scheme_name = match dep, lft2rgt, (cls = None) with
+    | false, true, true | false, false, false -> rew_l2r_scheme_kind
+    | false, false, true | false, true, false -> rew_r2l_scheme_kind
+    | true, true, true -> rew_l2r_dep_scheme_kind
+    | true, true, false -> rew_r2l_forward_dep_scheme_kind
+    | true, false, true -> rew_r2l_dep_scheme_kind
+    | true, false, false -> rew_l2r_forward_dep_scheme_kind
+  in
+  match kind_of_term hdcncl with
+  | Ind ind -> mkConst (find_scheme scheme_name ind)
+  | _ -> assert false
+
+let type_of_clause gl = function
+  | None -> pf_concl gl
+  | Some id -> pf_get_hyp_typ gl id
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars gl hdcncl =
-  let elim = find_elim hdcncl lft2rgt cls gl in
-  general_elim_clause with_evars tac cls sigma c t l lft2rgt (elim,NoBindings) gl
+  let dep = occur_term c (type_of_clause gl cls) in
+  let elim = find_elim hdcncl lft2rgt dep cls in
+  general_elim_clause with_evars tac cls sigma c t l lft2rgt
+    {elimindex = None; elimbody = (elim,NoBindings)} gl
 
 let adjust_rewriting_direction args lft2rgt =
-  if List.length args = 1 then
+  if List.length args = 1 then begin
     (* equality to a constant, like in eq_true *)
     (* more natural to see -> as the rewriting to the constant *)
+    if not lft2rgt then
+      error "Rewriting non-symmetric equality not allowed from right-to-left.";
     not lft2rgt
+  end
   else
     (* other equality *)
     lft2rgt
 
 let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
+(* Main function for dispatching which kind of rewriting it is about *)
+
 let general_rewrite_ebindings_clause cls lft2rgt occs ?tac
     ((c,l) : open_constr with_bindings) with_evars gl =
   if occs <> all_occurrences then (
@@ -206,7 +225,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?tac
     let ctype = get_type_of env sigma c' in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
-      | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
+      | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels)
 	    l with_evars gl hdcncl
@@ -949,6 +968,8 @@ let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
 
 exception Not_dep_pair
 
+let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
+let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -980,7 +1001,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
 (* and compare the fst arguments of the dep pair *)
         let new_eq_args = [|type_of env sigma (ar1.(3));ar1.(3);ar2.(3)|] in
         if ( (eqTypeDest = sigTconstr()) &&
-             (Ind_tables.check_dec_proof ind=true) &&
+             (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind=true) &&
              (is_conv env sigma (ar1.(2)) (ar2.(2)) = true))
               then (
 (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
@@ -991,7 +1012,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
               tclTHENS (cut (mkApp (ceq,new_eq_args)) )
                [tclIDTAC; tclTHEN (apply (
                   mkApp(inj2,
-                        [|ar1.(0);Ind_tables.find_eq_dec_proof ind;
+                        [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
                           ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
                   )) (Auto.trivial [] [])
                 ]
@@ -1048,7 +1069,7 @@ let swapEquandsInConcl gls =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim lbeq.eq false None gls in
+  let eq_elim = find_elim lbeq.eq false false None in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 7b63099c7..8c43888fb 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -25,6 +25,7 @@ open Tacexpr
 open Termops
 open Rawterm
 open Genarg
+open Ind_tables
 (*i*)
 
 type orientation = bool
@@ -137,3 +138,5 @@ val subst_all : ?strict:bool -> tactic
    (according to [dir] if given to get the rewrite direction)  in the clause [cl]
 *)
 val replace_multi_term : bool option -> constr -> clause -> tactic
+
+val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index b2824fbfb..9aec0e091 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -262,18 +262,16 @@ let match_with_equation t =
         else raise NoEquationFound
     | _ -> raise NoEquationFound
 
+let is_inductive_equality ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let nconstr = Array.length mip.mind_consnames in
+  nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
+
 let match_with_equality_type t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
-    | Ind ind when args <> [] ->
-        let (mib,mip) = Global.lookup_inductive ind in
-        let nconstr = Array.length mip.mind_consnames in
-	if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
-        then
-	  Some (hdapp,args)
-        else
-	  None
-    | _ -> None
+  | Ind ind when is_inductive_equality ind -> Some (hdapp,args)
+  | _ -> None
 
 let is_equality_type t = op2bool (match_with_equality_type t)
 
@@ -356,6 +354,7 @@ let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
 let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
 let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
+let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
 
 let match_eq eqn eq_pat =
   let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
@@ -388,9 +387,16 @@ let find_eq_data_decompose gl eqn =
   let (lbeq,eq_args) = find_eq_data eqn in
   (lbeq,extract_eq_args gl eq_args)
 
+let inversible_equalities =
+  [coq_eq_pattern, build_coq_inversion_eq_data;
+   coq_jmeq_pattern, build_coq_inversion_jmeq_data;
+   coq_identity_pattern, build_coq_inversion_identity_data;
+   coq_eq_true_pattern, build_coq_inversion_eq_true_data]
+
 let find_this_eq_data_decompose gl eqn =
   let (lbeq,eq_args) =
-    try find_eq_data eqn
+    try (*first_match (match_eq eqn) inversible_equalities*)
+      find_eq_data eqn
     with PatternMatchingFailure ->
       errorlabstrm "" (str "No primitive equality found.") in
   let eq_args =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 001755b1e..d98d2a2b3 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -83,6 +83,7 @@ val is_unit_or_eq_type     : testing_function
 val is_unit_type           : testing_function
 
 (* type with only one constructor, no arguments and at least one dependency *)
+val is_inductive_equality  : inductive -> bool
 val match_with_equality_type : (constr * constr list) matching_function
 val is_equality_type       : testing_function
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 67b699782..cd2a14236 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1285,7 +1285,7 @@ let add_morphism_infer glob m n =
       let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	Flags.silently
 	  (fun () ->
-	    Command.start_proof instance_id kind instance
+	    Lemmas.start_proof instance_id kind instance
 	      (fun _ -> function
 		Libnames.ConstRef cst ->
 		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a20fe72ef..332855052 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -377,10 +377,12 @@ let gl_make_elim ind gl =
   Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
 
 let gl_make_case_dep ind gl =
-  pf_apply Indrec.make_case_dep gl ind (elimination_sort_of_goal gl)
+  pf_apply Indrec.build_case_analysis_scheme gl ind true
+    (elimination_sort_of_goal gl)
 
 let gl_make_case_nodep ind gl =
-  pf_apply Indrec.make_case_nodep gl ind (elimination_sort_of_goal gl)
+  pf_apply Indrec.build_case_analysis_scheme gl ind false
+    (elimination_sort_of_goal gl)
 
 let elimination_then_using tac predicate bindings c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 97006c9e9..368502d40 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -692,6 +692,23 @@ let last_arg c = match kind_of_term c with
       array_last cl
   | _ -> anomaly "last_arg"
 
+let nth_arg i c =
+  if i = -1 then last_arg c else
+  match kind_of_term c with
+  | App (f,cl) -> cl.(i)
+  | _ -> anomaly "nth_arg"
+
+let index_of_ind_arg t =
+  let rec aux i j t = match kind_of_term t with
+  | Prod (_,t,u) ->
+      (* heuristic *)
+      if isInd (fst (decompose_app t)) then aux (Some j) (j+1) u
+      else aux i (j+1) u
+  | _ -> match i with
+      | Some i -> i
+      | None -> error "Could not find inductive argument of elimination scheme."
+  in aux None 0 t
+
 let elim_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
@@ -700,9 +717,9 @@ let elim_flags = {
   use_evars_pattern_unification = true;
 }
 
-let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
+let elimination_clause_scheme with_evars allow_K i elimclause indclause gl =
   let indmv =
-    (match kind_of_term (last_arg elimclause.templval.rebus) with
+    (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              (str "The type of elimination clause is not well-formed."))
@@ -719,16 +736,24 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
  * matching I, lbindc are the expected terms for c arguments
  *)
 
-let general_elim_clause_gen elimtac indclause (elimc,lbindelimc) gl =
-  let elimt      = pf_type_of gl elimc in
+type eliminator = {
+  elimindex : int option;  (* None = find it automatically *)
+  elimbody : constr with_ebindings
+}
+
+let general_elim_clause_gen elimtac indclause elim gl =
+  let (elimc,lbindelimc) = elim.elimbody in
+  let elimt = pf_type_of gl elimc in
+  let i =
+    match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
-    elimtac elimclause indclause gl
+  elimtac i elimclause indclause gl
 
-let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
+let general_elim_clause elimtac (c,lbindc) elim gl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
-    general_elim_clause_gen elimtac indclause (elimc,lbindelimc) gl
+    general_elim_clause_gen elimtac indclause elim gl
 
 let general_elim with_evars c e ?(allow_K=true) =
   general_elim_clause (elimination_clause_scheme with_evars allow_K) c e
@@ -738,13 +763,16 @@ let general_elim with_evars c e ?(allow_K=true) =
 
 let find_eliminator c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  lookup_eliminator ind (elimination_sort_of_goal gl)
+  let c = lookup_eliminator ind (elimination_sort_of_goal gl) in
+  {elimindex = None; elimbody = (c,NoBindings)}
 
 let default_elim with_evars (c,_ as cx) gl =
-  general_elim with_evars cx (find_eliminator c gl,NoBindings) gl
+  general_elim with_evars cx (find_eliminator c gl) gl
 
 let elim_in_context with_evars c = function
-  | Some elim -> general_elim with_evars c elim ~allow_K:true
+  | Some elim ->
+      general_elim with_evars c {elimindex = Some (-1); elimbody = elim}
+	~allow_K:true
   | None -> default_elim with_evars c
 
 let elim with_evars (c,lbindc as cx) elim =
@@ -774,11 +802,13 @@ let clenv_fchain_in id elim_flags mv elimclause hypclause =
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,NoOccurrenceFound (op,Some id)))
 
-let elimination_in_clause_scheme with_evars id elimclause indclause gl =
-  let (hypmv,indmv) =
-    match clenv_independent elimclause with
-        [k1;k2] -> (k1,k2)
-      | _  -> errorlabstrm "elimination_clause"
+let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
+  let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
+  let hypmv =
+    try match list_remove indmv (clenv_independent elimclause) with
+      | [a] -> a
+      | _ -> failwith ""
+    with Failure _ -> errorlabstrm "elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain indmv elimclause indclause in
   let hyp = mkVar id in
@@ -799,11 +829,14 @@ let general_elim_in with_evars id =
 
 let general_case_analysis_in_context with_evars (c,lbindc) gl =
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sort     = elimination_sort_of_goal gl in
-  let case =
-    if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in
-  let elim     = pf_apply case gl mind sort in
-  general_elim with_evars (c,lbindc) (elim,NoBindings) gl
+  let sort = elimination_sort_of_goal gl in
+  let elim =
+    if occur_term c (pf_concl gl) then
+      pf_apply build_case_analysis_scheme gl mind true sort
+    else
+      pf_apply build_case_analysis_scheme_default gl mind sort in
+  general_elim with_evars (c,lbindc)
+    {elimindex = None; elimbody = (elim,NoBindings)} gl
 
 let general_case_analysis with_evars (c,lbindc as cx) =
   match kind_of_term c with
@@ -824,9 +857,10 @@ let descend_in_conjunctions with_evars tac exit c gl =
     | Some (_,_,isrec) ->
 	let n = (mis_constr_nargs mind).(0) in
 	let sort = elimination_sort_of_goal gl in
-	let elim = pf_apply make_case_gen gl mind sort in
+	let elim = pf_apply build_case_analysis_scheme_default gl mind sort in
 	tclTHENLAST
-	  (general_elim with_evars (c,NoBindings) (elim,NoBindings))
+	  (general_elim with_evars (c,NoBindings)
+	     {elimindex = None; elimbody = (elim,NoBindings)})
 	  (tclTHENLIST [
 	    tclDO n intro;
 	    onNLastHypsId n (fun l ->
@@ -2037,6 +2071,7 @@ type elim_scheme = {
   elimc: constr with_ebindings option;
   elimt: types;
   indref: global_reference option;
+  index: int;              (* index of the elimination type in the scheme *)
   params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;            (* number of parameters *)
   predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -2058,6 +2093,7 @@ let empty_scheme =
     elimc = None;
     elimt = mkProp;
     indref = None;
+    index = -1;
     params = [];
     nparams = 0;
     predicates = [];
@@ -2072,7 +2108,6 @@ let empty_scheme =
     farg_in_concl = false;
   }
 
-
 let make_base n id =
   if n=0 or n=1 then id
   else
@@ -2723,12 +2758,12 @@ let guess_elim isrec hyp0 gl =
   let elimc =
     if isrec then lookup_eliminator mind s
     else
-      let case =
-	if use_dependent_propositions_elimination () &&
-	   dependent_no_evar (mkVar hyp0) (pf_concl gl) 
-	then make_case_dep
-	else make_case_gen in
-      pf_apply case gl mind s in
+      if use_dependent_propositions_elimination () &&
+	dependent_no_evar (mkVar hyp0) (pf_concl gl)
+      then
+	pf_apply build_case_analysis_scheme gl mind true s
+      else
+	pf_apply build_case_analysis_scheme_default gl mind s in
   let elimt = pf_type_of gl elimc in
   ((elimc, NoBindings), elimt), mkInd mind
 
@@ -2745,8 +2780,8 @@ let find_elim isrec elim hyp0 gl =
 type scheme_signature =
     (identifier list * (elim_arg_kind * bool * identifier) list) array
 
-type eliminator =
-  | ElimUsing of (constr with_ebindings * constr) * scheme_signature
+type eliminator_source =
+  | ElimUsing of (eliminator * types) * scheme_signature
   | ElimOver of bool * identifier
 
 let find_induction_type isrec elim hyp0 gl =
@@ -2758,10 +2793,11 @@ let find_induction_type isrec elim hyp0 gl =
 	(* We drop the scheme waiting to know if it is dependent *)
 	scheme, ElimOver (isrec,hyp0)
     | Some e ->
-	let (elimc,elimt as elim),ind_guess = given_elim hyp0 e gl in
+	let (elimc,elimt),ind_guess = given_elim hyp0 e gl in
 	let scheme = compute_elim_sig ~elimc elimt in
 	if scheme.indarg = None then error "Cannot find induction type";
 	let indsign = compute_scheme_signature scheme hyp0 ind_guess in
+	let elim = ({elimindex = Some(-1); elimbody = elimc},elimt) in
 	scheme, ElimUsing (elim,indsign) in
   Option.get scheme.indref,scheme.nparams, elim
 
@@ -2785,8 +2821,9 @@ let get_eliminator elim gl = match elim with
   | ElimUsing (elim,indsign) ->
       (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
-      let elim,_ as elims = guess_elim isrec id gl in
-      isrec, elim, fst (compute_elim_signature elims id)
+      let (elimc,elimt),_ as elims = guess_elim isrec id gl in
+      isrec, ({elimindex = None; elimbody = elimc}, elimt),
+      fst (compute_elim_signature elims id)
 
 (* Instantiate all meta variables of elimclause using lid, some elts
    of lid are parameters (first ones), the other are
@@ -2832,7 +2869,7 @@ let recolle_clenv nparams lid elimclause gl =
     produce new ones). Then refine with the resulting term with holes.
 *)
 let induction_tac_felim with_evars indvars nparams elim gl =
-  let (elimc,lbindelimc),elimt = elim in
+  let {elimbody=(elimc,lbindelimc)},elimt = elim in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimclause =
     make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
@@ -2882,7 +2919,7 @@ let apply_induction_in_context hyp0 elim indvars names induct_tac gl =
    all args and params must be given, so we help a bit the unifier by
    making the "pattern" by hand before calling induction_tac_felim
    FIXME: REUNIF AVEC induction_tac_felim? *)
-let induction_from_context_l isrec with_evars elim_info lid names gl =
+let induction_from_context_l with_evars elim_info lid names gl =
   let indsign,scheme = elim_info in
   (* number of all args, counting farg and indarg if present. *)
   let nargs_indarg_farg = scheme.nargs
@@ -2919,19 +2956,20 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
     (* FIXME: Tester ca avec un principe dependant et non-dependant *)
     induction_tac_felim with_evars realindvars scheme.nparams elim
   ] in
-  let elim = ElimUsing ((Option.get scheme.elimc, scheme.elimt), indsign) in
+  let elim = ElimUsing (({elimindex = Some scheme.index; elimbody = Option.get scheme.elimc}, scheme.elimt), indsign) in
   apply_induction_in_context
     None elim (hyp0::indvars) names induct_tac gl
 
 (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the
    hypothesis on which the induction is made *)
-let induction_tac isrec with_evars elim (varname,lbind) typ gl =
-  let ((elimc,lbindelimc),elimt) = elim in
+let induction_tac with_evars elim (varname,lbind) typ gl =
+  let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in
   let indclause = make_clenv_binding gl (mkVar varname,typ) lbind  in
+  let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   let elimclause =
     make_clenv_binding gl
-      (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
-  elimination_clause_scheme with_evars true elimclause indclause gl
+      (mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in
+  elimination_clause_scheme with_evars true i elimclause indclause gl
 
 let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps gl =
@@ -2939,7 +2977,7 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
   let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
   let induct_tac elim = tclTHENLIST [
-    induction_tac isrec with_evars elim (hyp0,lbind) typ0;
+    induction_tac with_evars elim (hyp0,lbind) typ0;
     tclTRY (unfold_body hyp0);
     thin [hyp0]
   ] in
@@ -2967,7 +3005,7 @@ let induction_without_atomization isrec with_evars elim names lid gl =
   let nlid = List.length lid in
   if nlid <> awaited_nargs
   then error "Not the right number of induction arguments."
-  else induction_from_context_l isrec with_evars elim_info lid names gl
+  else induction_from_context_l with_evars elim_info lid names gl
 
 let enforce_eq_name id gl = function
   | (b,(loc,IntroAnonymous)) ->
@@ -3177,8 +3215,7 @@ let elim_type t gl =
 
 let case_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let env = pf_env gl in
-  let elimc = make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in
+  let elimc = pf_apply build_case_analysis_scheme_default gl ind (elimination_sort_of_goal gl) in
   elim_scheme_type elimc t gl
 
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7d65ab752..19c0ba333 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -230,6 +230,7 @@ type elim_scheme = {
   elimc: constr with_ebindings option;
   elimt: types;
   indref: global_reference option;
+  index: int;              (* index of the elimination type in the scheme *)
   params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;            (* number of parameters *)
   predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -250,19 +251,25 @@ type elim_scheme = {
 val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
 val rebuild_elimtype_from_scheme: elim_scheme -> types
 
+(* elim principle with the index of its inductive arg *)
+type eliminator = {
+  elimindex : int option;  (* None = find it automatically *)
+  elimbody : constr with_ebindings
+}
+
 val elimination_clause_scheme : evars_flag ->
-  bool -> clausenv -> clausenv -> tactic
+  bool -> int -> clausenv -> clausenv -> tactic
 
-val elimination_in_clause_scheme : evars_flag -> identifier ->
+val elimination_in_clause_scheme : evars_flag -> identifier -> int ->
   clausenv -> clausenv -> tactic
 
-val general_elim_clause_gen : (Clenv.clausenv -> 'a -> tactic) ->
-  'a -> constr * open_constr bindings -> tactic
+val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
+  'a -> eliminator -> tactic
 
 val general_elim  : evars_flag ->
-  constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic
+  constr with_ebindings -> eliminator -> ?allow_K:bool -> tactic
 val general_elim_in : evars_flag ->
-  identifier -> constr with_ebindings -> constr with_ebindings -> tactic
+  identifier -> constr with_ebindings -> eliminator -> tactic
 
 val default_elim  : evars_flag -> constr with_ebindings -> tactic
 val simplest_elim : constr -> tactic
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0a0cfb79b..8c02e4662 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -10,6 +10,7 @@ Elim
 Dhyp
 Auto
 Ind_tables
+Eqschemes
 Equality
 Contradiction
 Inv
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 86e55922d..b06718251 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -38,3 +38,33 @@ Goal forall n, 0 + n = n -> True.
 intros n H.
 rewrite plus_0_l in H.
 Abort.
+
+(* Dependent rewrite from left-to-right *)
+
+Lemma l1 :
+  forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+
+(* Dependent rewrite from right-to-left *)
+
+Lemma l2 :
+  forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite <- H.
+rewrite <- H in H0.
+assumption.
+Qed.
+
+(* Check dependent rewriting with non-symmetric equalities *)
+
+Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H.
+intros x H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 127be1134..83edf434e 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -80,9 +80,9 @@ intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
 Lemma JMeq_congr :
- forall (A B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y).
+ forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
 Proof.
-intros A B f x y H; case JMeq_eq with (1 := H); trivial.
+intros A x B f y H; case JMeq_eq with (1 := H); trivial.
 Qed.
 
 (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5a21b9090..84f3420f2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -8,6 +8,9 @@
 
 (*i $Id$ i*)
 
+(* This file is about the automatic generation of schemes about
+   decidable equality, created by Vincent Siles, Oct 2007 *)
+
 open Tacmach
 open Util
 open Flags
@@ -28,7 +31,8 @@ open Tactics
 open Tacticals
 open Ind_tables
 
-(* boolean equality *)
+(**********************************************************************)
+(* Generic synthesis of boolean equality *)
 
 let quick_chop n l =
   let rec kick_last = function
@@ -47,13 +51,13 @@ let rec deconstruct_type t =
   let l,r = decompose_prod t in
     (List.map (fun (_,b) -> b) (List.rev l))@[r]
 
-let subst_in_constr (subst,(ind,const)) = 
-  let ind' = (subst_ind subst (fst ind)),(snd ind)
-  and const' = subst_mps subst const in
-    ind',const'
-
-exception EqNotFound of string
+exception EqNotFound of inductive * inductive
 exception EqUnknown of string
+exception UndefinedCst of string
+exception InductiveWithProduct
+exception InductiveWithSort
+exception ParameterWithoutEquality of constant
+exception NonSingletonProp of inductive
 
 let dl = dummy_loc
 
@@ -88,11 +92,18 @@ let mkFullInd ind n =
       Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
     else mkInd ind
 
-let make_eq_scheme sp =
+let check_bool_is_defined () =
+  try let _ = Global.type_of_global Coqlib.glob_bool in ()
+  with _ -> raise (UndefinedCst "bool")
+
+let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
+
+let build_beq_scheme kn =
+  check_bool_is_defined ();
   (* fetching global env *)
   let env = Global.env() in
   (* fetching the mutual inductive body *)
-  let mib = Global.lookup_mind sp in
+  let mib = Global.lookup_mind kn in
   (* number of inductives in the mutual *)
   let nb_ind = Array.length mib.mind_packets in
   (* number of params in the type *)
@@ -135,7 +146,7 @@ let make_eq_scheme sp =
                 t  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
-  let ind = sp,cur in
+  let ind = kn,cur in
   (* current inductive we are working on *)
   let cur_packet = mib.mind_packets.(snd ind) in
   (* Inductive toto : [rettyp] := *)
@@ -151,31 +162,34 @@ let make_eq_scheme sp =
     *)
     let compute_A_equality rel_list nlist eqA ndx t =
       let lifti = ndx in
-      let rec aux c a = match c with
+      let rec aux c =
+	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
+	match kind_of_term c with
         | Rel x -> mkRel (x-nlist+ndx)
         | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x)))
-        | Cast (x,_,_) -> aux (kind_of_term x) a
-        | App (x,newa) -> aux (kind_of_term x) newa
-        | Ind (sp',i) -> if eq_mind sp sp' then mkRel(eqA-nlist-i+nb_ind-1)
+        | Cast (x,_,_) -> aux (applist (x,a))
+        | App _ -> assert false
+        | Ind (kn',i as ind') -> if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
                         else ( try
-                          let eq = find_eq_scheme (sp',i)
-                          and eqa = Array.map
-                                (fun x -> aux (kind_of_term x) [||] ) a
-                          in
+			  let a = Array.of_list a in
+                          let eq = mkConst (find_scheme (!beq_scheme_kind_aux()) (kn',i))
+                          and eqa = Array.map aux a
+			  in
                             let args = Array.append
                                 (Array.map (fun x->lift lifti x) a) eqa
                             in if args = [||] then eq
                                else mkApp (eq,Array.append
                                       (Array.map (fun x->lift lifti x) a) eqa)
-                         with Not_found -> raise(EqNotFound (string_of_mind sp'))
+                         with Not_found -> raise(EqNotFound (ind',ind))
                         )
-        | Sort _  -> raise (EqUnknown "Sort" )
-        | Prod _ -> raise (EqUnknown "Prod" )
+        | Sort _  -> raise InductiveWithSort
+        | Prod _ -> raise InductiveWithProduct
         | Lambda _-> raise (EqUnknown "Lambda")
         | LetIn _ -> raise (EqUnknown "LetIn")
-        | Const kn -> let mp,dir,lbl= repr_con kn in
-                  mkConst (make_con mp dir (
-                                mk_label ("eq_"^(string_of_label lbl))))
+        | Const kn ->
+	    (match Environ.constant_opt_value env kn with
+	      | None -> raise (ParameterWithoutEquality kn)
+	      | Some c -> aux (applist (c,a)))
         | Construct _ -> raise (EqUnknown "Construct")
         | Case _ -> raise (EqUnknown "Case")
         | CoFix _ -> raise (EqUnknown "CoFix")
@@ -183,7 +197,7 @@ let make_eq_scheme sp =
         | Meta _  -> raise (EqUnknown "Meta")
         | Evar _  -> raise (EqUnknown "Evar")
     in
-      aux t [||]
+      aux t
   in
   (* construct the predicate for the Case part*)
   let do_predicate rel_list n =
@@ -217,7 +231,7 @@ let make_eq_scheme sp =
                                           nparrec
                                           (nparrec+3+2*nb_cstr_args)
                                           (nb_cstr_args+ndx+1)
-                                          (kind_of_term cc)
+                                          cc
                           in
                           Array.set eqs ndx
                               (mkApp (eqA,
@@ -245,40 +259,39 @@ let make_eq_scheme sp =
         mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2))  (
  	    mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar)))
-    in (* make_eq_scheme *)
-    try
+    in (* build_beq_scheme *)
     let names = Array.make nb_ind Anonymous and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet and
         res   = Array.make nb_ind mkSet in
     for i=0 to (nb_ind-1) do
         names.(i) <- Name (id_of_string (rec_name i));
-    	types.(i) <- mkArrow (mkFullInd (sp,i) 0)
-                     (mkArrow (mkFullInd (sp,i) 1) bb);
+	types.(i) <- mkArrow (mkFullInd (kn,i) 0)
+                     (mkArrow (mkFullInd (kn,i) 1) bb);
         cores.(i) <- make_one_eq i
     done;
-    if (string_of_mp (mind_modpath sp ))="Coq.Init.Logic"
+    if (string_of_mp (mind_modpath kn))="Coq.Init.Logic"
     then print_string "Logic time, do nothing.\n"
     else (
       for i=0 to (nb_ind-1) do
       let cpack = Array.get mib.mind_packets i in
-      if check_eq_scheme (sp,i)
+      if check_scheme (!beq_scheme_kind_aux()) (kn,i)
       then  message ("Boolean equality is already defined on "^
              (string_of_id cpack.mind_typename)^".")
       else (
+	let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
+	if not (List.mem InSet kelim) then
+	  raise (NonSingletonProp (kn,i));
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
           res.(i) <- create_input fix
         )
         done;
       );
       res
-      with
-        | EqUnknown s -> error ("Type unexpected ("^s^
-                  ") during boolean eq computation, please report.")
-        | EqNotFound s  -> error ("Boolean equality on "^s^
-          " is missing, equality will not be defined.")
-        | _ -> error ("Unknown exception during boolean equality creation,"^
-                      " the equality will not be defined.")
+
+let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
+
+let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
 
 (* This function tryies to get the [inductive] between a constr
   the constr should be Ind i or App(Ind i,[|args|])
@@ -291,7 +304,7 @@ let destruct_ind c =
             indc,[||]
 
 (*
-  In the followind, avoid is the list of names to avoid.
+  In the following, avoid is the list of names to avoid.
   If the args of the Inductive type are A1 ... An
   then avoid should be
  [| lb_An ... lb _A1  (resp. bl_An ... bl_A1)
@@ -299,7 +312,7 @@ let destruct_ind c =
 so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
-let do_replace_lb aavoid narg gls p q =
+let do_replace_lb lb_scheme_key aavoid narg gls p q =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -325,7 +338,7 @@ let do_replace_lb aavoid narg gls p q =
   let type_of_pq = pf_type_of gls p in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
-        try find_lb_proof u
+        try mkConst (find_scheme lb_scheme_key u)
         with Not_found ->
           (* spiwack: the format of this error message should probably
 	              be improved. *)
@@ -346,9 +359,8 @@ let do_replace_lb aavoid narg gls p q =
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
             in [Equality.replace p q ; apply app ; Auto.default_auto]
 
-
 (* used in the bool -> leib side *)
-let do_replace_bl ind gls aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -384,7 +396,7 @@ let do_replace_bl ind gls aavoid narg lft rgt =
              then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
              else (
                let bl_t1 =
-               try find_bl_proof u
+               try mkConst (find_scheme bl_scheme_key u)
                with Not_found ->
 		 (* spiwack: the format of this error message should probably
 	                     be improved. *)
@@ -449,11 +461,14 @@ let eqI ind l =
   let list_id = list_id l in
   let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
-  and  e = try find_eq_scheme ind  with
+  and  e = try mkConst (find_scheme beq_scheme_kind ind) with
     Not_found -> error
         ("The boolean equality on "^(string_of_mind (fst ind))^" is needed.");
   in (if eA = [||] then e else mkApp(e,eA))
 
+(**********************************************************************)
+(* Boolean->Leibniz *)
+
 let compute_bl_goal ind lnamesparrec nparrec =
   let eqI = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
@@ -481,8 +496,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
                 (match n with Name s -> s | Anonymous ->  id_of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "n" and
-          m = id_of_string "m" in
+      let n = id_of_string "x" and
+          m = id_of_string "y" in
      create_input (
         mkNamedProd n (mkFullInd ind nparrec) (
           mkNamedProd m (mkFullInd ind (nparrec+1)) (
@@ -491,10 +506,9 @@ let compute_bl_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|]))
         )))
 
-let compute_bl_tact ind lnamesparrec nparrec  =
+let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
   let list_id = list_id lnamesparrec in
   let avoid = ref [] in
-    let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
       let first_intros =
         ( List.map (fun (s,_,_,_) -> s ) list_id ) @
         ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @
@@ -503,14 +517,13 @@ let compute_bl_tact ind lnamesparrec nparrec  =
       let fresh_first_intros = List.map ( fun s ->
         let fresh = fresh_id (!avoid) s gsig in
         avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
+      let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
       let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (id_of_string "m") gsig in
+            fresh_id (!avoid) (id_of_string "y") gsig in
       let freshz = avoid := freshm::(!avoid);
             fresh_id (!avoid) (id_of_string "Z") gsig in
   (* try with *)
       avoid := freshz::(!avoid);
-      Pfedit.by (
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
@@ -555,10 +568,11 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                       match (kind_of_term gl) with
                       | App (c,ca) -> (
                         match (kind_of_term c) with
-                        | Ind (i1,i2) ->
-                            if(string_of_label (mind_label i1) = "eq")
+                        | Ind indeq ->
+                            if IndRef indeq = Coqlib.glob_eq
                             then (
-                              tclTHENSEQ ((do_replace_bl ind gls (!avoid)
+                              tclTHENSEQ ((do_replace_bl bl_scheme_key ind gls
+				                      (!avoid)
                                                       nparrec (ca.(2))
                               (ca.(1)))@[Auto.default_auto]) gls
                             )
@@ -568,8 +582,30 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                       )
                       | _ -> error "Failure while solving Boolean->Leibniz."
 
-                    ]
-      )
+                    ] gsig
+
+let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
+
+let make_bl_scheme mind =
+  let mib = Global.lookup_mind mind in
+  if Array.length mib.mind_packets <> 1 then
+    errorlabstrm ""
+      (str "Automatic building of boolean->Leibniz lemmas not supported");
+  let ind = (mind,0) in
+  let nparams = mib.mind_nparams in
+  let nparrec = mib.mind_nparams_rec in
+  let lnonparrec,lnamesparrec =
+    context_chop (nparams-nparrec) mib.mind_params_ctxt in
+  [|Pfedit.build_by_tactic
+    (compute_bl_goal ind lnamesparrec nparrec)
+    (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|]
+
+let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
+
+let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
+
+(**********************************************************************)
+(* Leibniz->Boolean *)
 
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
@@ -598,8 +634,8 @@ let compute_lb_goal ind lnamesparrec nparrec =
                 (match n with Name s -> s | Anonymous ->  id_of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "n" and
-          m = id_of_string "m" in
+      let n = id_of_string "x" and
+          m = id_of_string "y" in
       create_input (
         mkNamedProd n (mkFullInd ind nparrec) (
           mkNamedProd m (mkFullInd ind (nparrec+1)) (
@@ -608,10 +644,9 @@ let compute_lb_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
         )))
 
-let compute_lb_tact ind lnamesparrec nparrec =
+let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
-    let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
       let first_intros =
         ( List.map (fun (s,_,_,_) -> s ) list_id ) @
         ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
@@ -620,14 +655,13 @@ let compute_lb_tact ind lnamesparrec nparrec =
       let fresh_first_intros = List.map ( fun s ->
         let fresh = fresh_id (!avoid) s gsig in
         avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
+      let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
       let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (id_of_string "m") gsig in
+            fresh_id (!avoid) (id_of_string "y") gsig in
       let freshz = avoid := freshm::(!avoid);
             fresh_id (!avoid) (id_of_string "Z") gsig in
   (* try with *)
       avoid := freshz::(!avoid);
-      Pfedit.by (
       tclTHENSEQ [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      new_induct false [Tacexpr.ElimOnConstr
@@ -659,7 +693,8 @@ let compute_lb_tact ind lnamesparrec nparrec =
                           | App(c,ca) -> (match (kind_of_term ca.(1)) with
                               | App(c',ca') ->
                                   let n = Array.length ca' in
-                                    tclTHENSEQ (do_replace_lb (!avoid)
+                                    tclTHENSEQ (do_replace_lb lb_scheme_key
+				                (!avoid)
                                                 nparrec gls
                                                 ca'.(n-2) ca'.(n-1)) gls
                               | _ -> error
@@ -667,11 +702,37 @@ let compute_lb_tact ind lnamesparrec nparrec =
                             )
                           | _ -> error
                                   "Failure while solving Leibniz->Boolean."
-                    ]
-            )
+                    ] gsig
+
+let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
+
+let make_lb_scheme mind =
+  let mib = Global.lookup_mind mind in
+  if Array.length mib.mind_packets <> 1 then
+    errorlabstrm ""
+      (str "Automatic building of Leibniz->boolean lemmas not supported");
+  let ind = (mind,0) in
+  let nparams = mib.mind_nparams in
+  let nparrec = mib.mind_nparams_rec in
+  let lnonparrec,lnamesparrec =
+    context_chop (nparams-nparrec) mib.mind_params_ctxt in
+  [|Pfedit.build_by_tactic
+    (compute_lb_goal ind lnamesparrec nparrec)
+    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|]
+
+let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
+
+let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
+
+(**********************************************************************)
+(* Decidable equality *)
+
+let check_not_is_defined () =
+  try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not")
 
 (* {n=m}+{n<>m}  part  *)
 let compute_dec_goal ind lnamesparrec nparrec =
+  check_not_is_defined ();
   let list_id = list_id lnamesparrec in
     let create_input c =
       let x = id_of_string "x" and
@@ -710,8 +771,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
                 (match n with Name s -> s | Anonymous ->  id_of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "n" and
-          m = id_of_string "m" in
+      let n = id_of_string "x" and
+          m = id_of_string "y" in
         let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
@@ -721,93 +782,116 @@ let compute_dec_goal ind lnamesparrec nparrec =
         )
       )
 
-let compute_dec_tact ind lnamesparrec nparrec =
+let compute_dec_tact ind lnamesparrec nparrec gsig =
   let list_id = list_id lnamesparrec in
   let eqI = eqI ind lnamesparrec in
-    let avoid = ref [] in
-    let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
-    let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
-    let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
-      let first_intros =
-        ( List.map (fun (s,_,_,_) -> s ) list_id ) @
-        ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
-        ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
-        ( List.map (fun (_,_,_,slb) -> slb) list_id )
-      in
-      let fresh_first_intros = List.map ( fun s ->
-        let fresh = fresh_id (!avoid) s gsig in
-        avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
-      let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (id_of_string "m") gsig in
-      let freshH = avoid := freshm::(!avoid);
-            fresh_id (!avoid) (id_of_string "H") gsig in
-      let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
-      avoid := freshH::(!avoid);
-      Pfedit.by ( tclTHENSEQ [
-                        intros_using fresh_first_intros;
-                        intros_using [freshn;freshm];
-                        assert_tac (Name freshH) (
-                        mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
-                  ) ]);
-(*we do this so we don't have to prove the same goal twice *)
-      Pfedit.by (  tclTHEN
-                   (new_destruct false [Tacexpr.ElimOnConstr
-                                  (eqbnm,Rawterm.NoBindings)]
-                                None
-                                (None,None)
-		                None)
-                  Auto.default_auto
-                );
-      Pfedit.by (
-                  let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
-                    avoid := freshH2::(!avoid);
-                    new_destruct false [Tacexpr.ElimOnConstr
-                                    ((mkVar freshH),Rawterm.NoBindings)]
-                                None
-                                (None,Some (dl,Genarg.IntroOrAndPattern [
-                                    [dl,Genarg.IntroAnonymous];
-                                    [dl,Genarg.IntroIdentifier freshH2]])) None
-      );
-      let arfresh = Array.of_list fresh_first_intros in
-        let xargs = Array.sub arfresh 0 (2*nparrec) in
-          let blI = try find_bl_proof ind with
+  let avoid = ref [] in
+  let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
+  let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
+  let first_intros =
+      ( List.map (fun (s,_,_,_) -> s ) list_id ) @
+      ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
+      ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
+      ( List.map (fun (_,_,_,slb) -> slb) list_id )
+  in
+  let fresh_first_intros = List.map ( fun s ->
+    let fresh = fresh_id (!avoid) s gsig in
+    avoid := fresh::(!avoid); fresh ) first_intros in
+  let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
+  let freshm = avoid := freshn::(!avoid);
+    fresh_id (!avoid) (id_of_string "y") gsig in
+  let freshH = avoid := freshm::(!avoid);
+    fresh_id (!avoid) (id_of_string "H") gsig in
+  let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
+  avoid := freshH::(!avoid);
+  let arfresh = Array.of_list fresh_first_intros in
+  let xargs = Array.sub arfresh 0 (2*nparrec) in
+  let blI = try mkConst (find_scheme bl_scheme_kind ind) with
             Not_found -> error (
               "Error during the decidability part, boolean to leibniz"^
               " equality is required.")
-          in
-          let lbI = try find_lb_proof ind  with
+  in
+  let lbI = try mkConst (find_scheme lb_scheme_kind ind) with
             Not_found -> error (
               "Error during the decidability part, leibniz to boolean"^
               " equality is required.")
-          in
-
-      (* left *)
-          Pfedit.by ( tclTHENSEQ [ simplest_left;
-                          apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
-                          Auto.default_auto
-          ]);
-      (*right *)
-          let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in
-          avoid := freshH3::(!avoid);
-          Pfedit.by (tclTHENSEQ [ simplest_right ;
-                      unfold_constr (Lazy.force Coqlib.coq_not_ref);
-                      intro;
-                      Equality.subst_all;
-                assert_tac (Name freshH3)
-                (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
-          ]);
-          Pfedit.by
-            (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
-                      Auto.default_auto
-            ]);
-         Pfedit.by (Equality.general_rewrite_bindings_in true
+  in
+  tclTHENSEQ [
+        intros_using fresh_first_intros;
+        intros_using [freshn;freshm];
+	(*we do this so we don't have to prove the same goal twice *)
+        assert_by (Name freshH) (
+          mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+	)
+	  (tclTHEN
+	    (new_destruct false [Tacexpr.ElimOnConstr
+              (eqbnm,Rawterm.NoBindings)]
+              None
+              (None,None)
+	      None)
+	    Auto.default_auto);
+        (fun gsig ->
+	  let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
+          avoid := freshH2::(!avoid);
+	  tclTHENS (
+	    new_destruct false [Tacexpr.ElimOnConstr
+                                    ((mkVar freshH),Rawterm.NoBindings)]
+                                None
+                                (None,Some (dl,Genarg.IntroOrAndPattern [
+                                    [dl,Genarg.IntroAnonymous];
+                                    [dl,Genarg.IntroIdentifier freshH2]])) None
+	  ) [
+	    (* left *)
+	    tclTHENSEQ [
+	      simplest_left;
+              apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
+              Auto.default_auto
+            ];
+	    (*right *)
+            (fun gsig ->
+	    let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in
+            avoid := freshH3::(!avoid);
+            tclTHENSEQ [
+	      simplest_right ;
+              unfold_constr (Lazy.force Coqlib.coq_not_ref);
+              intro;
+              Equality.subst_all;
+              assert_by (Name freshH3)
+		(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
+		(tclTHENSEQ [
+		  apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
+                  Auto.default_auto
+		]);
+	      Equality.general_rewrite_bindings_in true
 	                      all_occurrences
                               (List.hd !avoid)
                               ((mkVar (List.hd (List.tl !avoid))),
                                 Rawterm.NoBindings
                               )
-                              true);
-        Pfedit.by (Equality.discr_tac false None)
+                              true;
+              Equality.discr_tac false None
+	    ] gsig)
+	  ] gsig)
+  ] gsig
+
+let make_eq_decidability mind =
+  let mib = Global.lookup_mind mind in
+  if Array.length mib.mind_packets <> 1 then
+    anomaly "Decidability lemma for mutual inductive types not supported";
+  let ind = (mind,0) in
+  let nparams = mib.mind_nparams in
+  let nparrec = mib.mind_nparams_rec in
+  let lnonparrec,lnamesparrec =
+    context_chop (nparams-nparrec) mib.mind_params_ctxt in
+  [|Pfedit.build_by_tactic
+    (compute_dec_goal ind lnamesparrec nparrec)
+    (compute_dec_tact ind lnamesparrec nparrec)|]
+
+let eq_dec_scheme_kind =
+  declare_mutual_scheme_object "_eq_dec" make_eq_decidability
 
+(* The eq_dec_scheme proofs depend on the equality and discr tactics
+   but the inj tactics, that comes with discr, depends on the
+   eq_dec_scheme... *)
 
+let _ = Equality.set_eq_dec_scheme_kind eq_dec_scheme_kind
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 5e8c1a07f..855f023f5 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -11,17 +11,31 @@ open Names
 open Libnames
 open Mod_subst
 open Sign
+open Proof_type
+open Ind_tables
 
+(* Build boolean equality of a block of mutual inductive types *)
 
-val subst_in_constr : (substitution*(inductive*constr))
-                     -> (inductive*constr)
+exception EqNotFound of inductive * inductive
+exception EqUnknown of string
+exception UndefinedCst of string
+exception InductiveWithProduct
+exception InductiveWithSort
+exception ParameterWithoutEquality of constant
+exception NonSingletonProp of inductive
 
-val compute_bl_goal : inductive -> rel_context -> int -> types
-val compute_bl_tact : inductive -> rel_context -> int -> unit
-val compute_lb_goal : inductive -> rel_context -> int -> types
-val compute_lb_tact : inductive -> rel_context -> int -> unit
-val compute_dec_goal : inductive -> rel_context -> int -> types
-val compute_dec_tact : inductive -> rel_context -> int -> unit
+val beq_scheme_kind : mutual scheme_kind
+val build_beq_scheme : mutual_inductive -> constr array
 
+(* Build equivalence between boolean equality and Leibniz equality *)
 
-val make_eq_scheme :mutual_inductive -> types array
+val lb_scheme_kind : mutual scheme_kind
+val make_lb_scheme : mutual_inductive -> constr array
+
+val bl_scheme_kind : mutual scheme_kind
+val make_bl_scheme : mutual_inductive -> constr array
+
+(* Build decidability of equality *)
+
+val eq_dec_scheme_kind : mutual scheme_kind
+val make_eq_decidability : mutual_inductive -> constr array
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index de2e78ba5..063fe7a10 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -74,7 +74,7 @@ type binder_list = (identifier located * bool * constr_expr) list
 
 (* Calls to interpretation functions. *)
 
-let interp_type_evars evdref env ?(impls=([],[])) typ =
+let interp_type_evars evdref env ?(impls=empty_internalization_env) typ =
   let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
@@ -129,7 +129,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     in DefinitionEntry entry, kind
   in
   let kn = Declare.declare_constant id cdecl in
-    Flags.if_verbose Command.definition_message id;
+    Declare.definition_message id;
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
@@ -254,7 +254,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
-		Command.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
+		Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
 		if props <> [] then 
 		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
 		    (!refine_ref (evm, term))
@@ -308,7 +308,7 @@ let context ?(hook=fun _ -> ()) l =
 	let impl = List.exists (fun (x,_) ->
 	  match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
 	in
-	  Command.declare_one_assumption false (Local (* global *), Definitional) t
+	  Command.declare_assumption false (Local (* global *), Definitional) t
 	    [] impl (* implicit *) false (* inline *) (dummy_loc, id);
 	  match class_of_constr t with
 	  | None -> ()
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 34afbbcd5..67660cab3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -13,54 +13,25 @@ open Util
 open Flags
 open Term
 open Termops
-open Declarations
 open Entries
-open Inductive
 open Environ
-open Reduction
 open Redexpr
 open Declare
-open Nametab
 open Names
 open Libnames
 open Nameops
 open Topconstr
-open Library
-open Libobject
 open Constrintern
-open Proof_type
-open Tacmach
-open Safe_typing
 open Nametab
 open Impargs
-open Typeops
 open Reductionops
 open Indtypes
-open Vernacexpr
 open Decl_kinds
 open Pretyping
 open Evarutil
 open Evarconv
 open Notation
-open Goptions
-open Mod_subst
-open Evd
-open Decls
-open Smartlocate
-
-let rec abstract_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,k,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl
-        (abstract_constr_expr c bl)
-
-let rec generalize_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
-  | LocalRawAssum (idl,k,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl
-        (generalize_constr_expr c bl)
+open Indschemes
 
 let rec under_binders env f n c =
   if n = 0 then f env Evd.empty c else
@@ -88,23 +59,30 @@ let rec complete_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
-let definition_message id =
-  if_verbose message ((string_of_id id) ^ " is defined")
+let red_constant_entry bl ce = function
+  | None -> ce
+  | Some red ->
+      let body = ce.const_entry_body in
+      { ce with const_entry_body =
+	under_binders (Global.env()) (fst (reduction_of_red_expr red))
+	  (local_binders_length bl)
+	  body }
 
-let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
+let interp_definition boxed bl red_option c ctypopt =
   let env = Global.env() in
-    match comtypopt with
+  let imps,ce =
+    match ctypopt with
       None ->
-	let b = abstract_constr_expr com bl in
+	let b = abstract_constr_expr c bl in
 	let b, imps = interp_constr_evars_impls env b in
 	  imps,
 	{ const_entry_body = b;
 	  const_entry_type = None;
-          const_entry_opaque = opacity;
+          const_entry_opaque = false;
 	  const_entry_boxed = boxed }
-    | Some comtyp ->
-	let ty = generalize_constr_expr comtyp bl in
-	let b = abstract_constr_expr com bl in
+    | Some ctyp ->
+	let ty = prod_constr_expr ctyp bl in
+	let b = abstract_constr_expr c bl in
 	let evdref = ref Evd.empty in
 	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env ty in
 	let b, imps = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env b ty in
@@ -114,20 +92,13 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	  imps,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
-          const_entry_opaque = opacity;
+          const_entry_opaque = false;
 	  const_entry_boxed = boxed }
+  in
+  red_constant_entry bl ce red_option, imps
 
-let red_constant_entry bl ce = function
-  | None -> ce
-  | Some red ->
-      let body = ce.const_entry_body in
-      { ce with const_entry_body =
-	under_binders (Global.env()) (fst (reduction_of_red_expr red))
-	  (local_binders_length bl)
-	  body }
-
-let declare_global_definition ident ce local imps =
-  let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
+let declare_global_definition ident ce local k imps =
+  let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in
   let gr = ConstRef kn in
     maybe_declare_manual_implicits false gr imps;
     if local = Local && Flags.is_verbose() then
@@ -140,15 +111,13 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
-  let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
-  let ce' = red_constant_entry bl ce red_option in
-  !declare_definition_hook ce';
+let declare_definition ident (local,k) ce imps hook =
+  !declare_definition_hook ce;
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let c =
-          SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
-        let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
+          SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
+        let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in
         definition_message ident;
         if Pfedit.refining () then
           Flags.if_verbose msg_warning
@@ -156,20 +125,12 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
              str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
-        declare_global_definition ident ce' local imps in
+        declare_global_definition ident ce local k imps in
   hook local r
 
-let syntax_definition ident (vars,c) local onlyparse =
-  let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in
-  let onlyparse = onlyparse or Metasyntax.is_not_printable pat in
-  Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
-
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let assumption_message id =
-  if_verbose message ((string_of_id id) ^ " is assumed")
-
-let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) =
+let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let _ =
@@ -193,286 +154,22 @@ let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) =
         gr in
   if is_coe then Class.try_add_new_coercion r local
 
-let declare_assumption_hook = ref ignore
-let set_declare_assumption_hook = (:=) declare_assumption_hook
-
-let declare_assumption idl is_coe k bl c impl nl =
-  if not (Pfedit.refining ()) then
-    let c = generalize_constr_expr c bl in
-    let env = Global.env () in
-    let c', imps = interp_type_evars_impls env c in
-      !declare_assumption_hook c';
-      List.iter (declare_one_assumption is_coe k c' imps impl nl) idl
-  else
-    errorlabstrm "Command.Assumption"
-	(str "Cannot declare an assumption while in proof editing mode.")
-
-(* 3a| Elimination schemes for mutual inductive definitions *)
-
-open Indrec
-open Inductiveops
+let declare_assumptions_hook = ref ignore
+let set_declare_assumptions_hook = (:=) declare_assumptions_hook
 
+let interp_assumption bl c =
+  let c = prod_constr_expr c bl in
+  let env = Global.env () in
+  interp_type_evars_impls env c
 
-let non_type_eliminations =
-  [ (InProp,elimination_suffix InProp);
-    (InSet,elimination_suffix InSet) ]
+let declare_assumptions idl is_coe k c imps impl_is_on nl =
+  !declare_assumptions_hook c;
+  List.iter (declare_assumption is_coe k c imps impl_is_on nl) idl
 
-let declare_one_elimination ind =
-  let (mib,mip) = Global.lookup_inductive ind in
-  let mindstr = string_of_id mip.mind_typename in
-  let declare s c t =
-    let id = id_of_string s in
-    let kn = Declare.declare_internal_constant id
-      (DefinitionEntry
-        { const_entry_body = c;
-          const_entry_type = t;
-          const_entry_opaque = false;
-	  const_entry_boxed = Flags.boxed_definitions() },
-       Decl_kinds.IsDefinition Definition) in
-    definition_message id;
-    kn
-  in
-  let env = Global.env () in
-  let sigma = Evd.empty in
-  let elim_scheme = Indrec.build_indrec env sigma ind in
-  let npars =
-    (* if a constructor of [ind] contains a recursive call, the scheme
-       is generalized only wrt recursively uniform parameters *)
-    if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs)
-    then
-      mib.mind_nparams_rec
-    else
-      mib.mind_nparams in
-  let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in
-  let kelim = elim_sorts (mib,mip) in
-    (* in case the inductive has a type elimination, generates only one
-       induction scheme, the other ones share the same code with the
-       apropriate type *)
-  if List.mem InType kelim then
-    let elim = make_elim (new_sort_in_family InType) in
-    let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in
-    let c = mkConst cte in
-    let t = type_of_constant (Global.env()) cte in
-    List.iter (fun (sort,suff) ->
-      let (t',c') =
-	Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort)
-	  npars c t in
-      let _ = declare (mindstr^suff) c' (Some t') in ())
-      non_type_eliminations
-   else (* Impredicative or logical inductive definition *)
-     List.iter
-    (fun (sort,suff) ->
-       if List.mem sort kelim then
-	 let elim = make_elim (new_sort_in_family sort) in
-	 let _ = declare (mindstr^suff) elim None in ())
-       non_type_eliminations
-
-(* bool eq declaration flag && eq dec declaration flag *)
-let eq_flag = ref false
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Scheme"];
-      optread  = (fun () -> !eq_flag) ;
-      optwrite = (fun b -> eq_flag := b) }
-
-(* boolean equality *)
-let (inScheme,_) =
-  declare_object {(default_object "EQSCHEME") with
-                    cache_function = Ind_tables.cache_scheme;
-                    load_function = (fun _ -> Ind_tables.cache_scheme);
-                    subst_function = Auto_ind_decl.subst_in_constr }
-
-let declare_eq_scheme sp =
-  let mib = Global.lookup_mind sp in
-  let nb_ind = Array.length mib.mind_packets in
-  let eq_array = Auto_ind_decl.make_eq_scheme sp in
-  try
-    for i=0 to (nb_ind-1) do
-    let cpack = Array.get mib.mind_packets i in
-    let nam = id_of_string ((string_of_id cpack.mind_typename)^"_beq")
-    in
-      let cst_entry = {const_entry_body = eq_array.(i);
-                       const_entry_type = None;
-                       const_entry_opaque = false;
-                       const_entry_boxed = Flags.boxed_definitions() }
-      in
-      let cst_decl =  (DefinitionEntry cst_entry),(IsDefinition Definition)
-      in
-        let cst = Declare.declare_constant nam cst_decl in
-          Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst));
-          definition_message nam
-    done
-  with Not_found ->
-    error "Your type contains Parameters without a boolean equality."
-
-(* decidability of eq *)
-
-
-let (inBoolLeib,_) =
-  declare_object {(default_object "BOOLLIEB") with
-                    cache_function = Ind_tables.cache_bl;
-                    load_function = (fun _ -> Ind_tables.cache_bl);
-                    subst_function = Auto_ind_decl.subst_in_constr }
-
-let (inLeibBool,_) =
-  declare_object {(default_object "LIEBBOOL") with
-                    cache_function = Ind_tables.cache_lb;
-                    load_function = (fun _ -> Ind_tables.cache_lb);
-                    subst_function = Auto_ind_decl.subst_in_constr }
-
-let (inDec,_) =
-  declare_object {(default_object "EQDEC") with
-                    cache_function = Ind_tables.cache_dec;
-                    load_function = (fun _ -> Ind_tables.cache_dec);
-                    subst_function = Auto_ind_decl.subst_in_constr }
-
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
-  let sign = Global.named_context () in
-  let sign = clear_proofs sign in
-  !start_hook c;
-  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
-
-let adjust_guardness_conditions const =
-  (* Try all combinations... not optimal *)
-  match kind_of_term const.const_entry_body with
-  | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-      let possible_indexes =
-	List.map (fun c ->
-	  interval 0 (List.length ((lam_assum c))))
-	  (Array.to_list fixdefs) in
-      let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
-      { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
-  | c -> const
-
-let save id const do_guard (locality,kind) hook =
-  let const = if do_guard then adjust_guardness_conditions const else const in
-  let {const_entry_body = pft;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
-  let k = logical_kind_of_goal_kind kind in
-  let l,r = match locality with
-    | Local when Lib.sections_are_opened () ->
-	let c = SectionLocalDef (pft, tpo, opacity) in
-	let _ = declare_variable id (Lib.cwd(), c, k) in
-	(Local, VarRef id)
-    | Local | Global ->
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	Autoinstance.search_declaration (ConstRef kn);
-	(Global, ConstRef kn) in
-  Pfedit.delete_current_proof ();
-  definition_message id;
-  hook l r
-
-let save_hook = ref ignore
-let set_save_hook f = save_hook := f
-
-let save_named opacity =
-  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
-  let const = { const with const_entry_opaque = opacity } in
-  save id const do_guard persistence hook
-
-let make_eq_decidability ind =
-    (* fetching data *)
-    let mib = Global.lookup_mind (fst ind) in
-    let nparams = mib.mind_nparams in
-    let nparrec = mib.mind_nparams_rec in
-    let lnonparrec,lnamesparrec =
-      context_chop (nparams-nparrec) mib.mind_params_ctxt in
-    let proof_name = (string_of_id(
-          Array.get mib.mind_packets (snd ind)).mind_typename)^"_eq_dec" in
-    let bl_name  =(string_of_id(
-          Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_bl" in
-    let lb_name  =(string_of_id(
-          Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_lb" in
-  (* main calls*)
-    if Ind_tables.check_bl_proof ind
-    then (message (bl_name^" is already declared."))
-    else (
-      start_proof (id_of_string bl_name)
-         (Global,Proof Theorem)
-         (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec)
-            (fun _ _ -> ());
-      Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec;
-      save_named true;
-      Lib.add_anonymous_leaf
-        (inBoolLeib (ind,mkConst (Lib.make_con (id_of_string bl_name))))
-(*        definition_message (id_of_string bl_name) *)
-    );
-    if Ind_tables.check_lb_proof ind
-    then (message (lb_name^" is already declared."))
-    else (
-      start_proof (id_of_string lb_name)
-        (Global,Proof Theorem)
-        (Auto_ind_decl.compute_lb_goal ind lnamesparrec nparrec)
-        ( fun _ _ -> ());
-      Auto_ind_decl.compute_lb_tact ind lnamesparrec nparrec;
-      save_named true;
-      Lib.add_anonymous_leaf
-        (inLeibBool (ind,mkConst (Lib.make_con (id_of_string lb_name))))
-(*      definition_message (id_of_string lb_name) *)
-    );
-    if Ind_tables.check_dec_proof ind
-    then (message (proof_name^" is already declared."))
-    else (
-      start_proof (id_of_string proof_name)
-        (Global,Proof Theorem)
-        (Auto_ind_decl.compute_dec_goal ind lnamesparrec nparrec)
-        ( fun _ _ -> ());
-      Auto_ind_decl.compute_dec_tact ind lnamesparrec nparrec;
-      save_named true;
-      Lib.add_anonymous_leaf
-        (inDec (ind,mkConst (Lib.make_con (id_of_string proof_name))))
-(*      definition_message (id_of_string proof_name) *)
-  )
-
-(* end of automated definition on ind*)
-
-let declare_eliminations sp =
-  let mib = Global.lookup_mind sp in
-  if mib.mind_finite then begin
-    if (!eq_flag) then (declare_eq_scheme sp);
-    for i = 0 to Array.length mib.mind_packets - 1 do
-      declare_one_elimination (sp,i);
-      try
-        if (!eq_flag) then (make_eq_decidability (sp,i))
-      with _ ->
-          Pfedit.delete_current_proof();
-          message "Error while computing decidability scheme. Please report."
-    done;
-  end
+(* 3a| Elimination schemes for mutual inductive definitions *)
 
 (* 3b| Mutual inductive definitions *)
 
-let compute_interning_datas env ty l nal typl impll =
-  let mk_interning_data na typ impls =
-    let idl, impl =
-      let impl =
-	compute_implicits_with_manual env typ (is_implicit_args ()) impls
-      in
-      let sub_impl,_ = list_chop (List.length l) impl in
-      let sub_impl' = List.filter is_status_implicit sub_impl in
-	(List.map name_of_implicit sub_impl', impl)
-    in
-      (na, (ty, idl, impl, compute_arguments_scope typ)) in
-  (l, list_map3 mk_interning_data nal typl impll)
-
-
- (* temporary open scopes during interpretation of mutual families
-    so that locally defined notations are available
- *)
-let open_temp_scopes =  function
-  | None -> ()
-  | Some sc -> if not (Notation.scope_is_open sc)
-     then Notation.open_close_scope (false,true,sc)
-
-let declare_interning_data (_,impls) (df,c,scope) =
-  silently (Metasyntax.add_notation_interpretation df impls c) scope
-
 let push_named_types env idl tl =
   List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env)
     env idl tl
@@ -481,12 +178,15 @@ let push_types env idl tl =
   List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env)
     env idl tl
 
-type inductive_expr = {
+type structured_one_inductive_expr = {
   ind_name : identifier;
   ind_arity : constr_expr;
   ind_lc : (identifier * constr_expr) list
 }
 
+type structured_inductive_expr =
+  local_binder list * structured_one_inductive_expr list
+
 let minductive_message = function
   | []  -> error "No inductive definition."
   | [x] -> (pr_id x ++ str " is defined")
@@ -522,7 +222,7 @@ let interp_cstrs evdref env impls mldata arity ind =
   let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in
     (cnames, ctyps'', cimpls)
 
-let interp_mutual paramsl indl notations finite =
+let interp_mutual_inductive (paramsl,indl) notations finite =
   check_all_names_different indl;
   let env0 = Global.env() in
   let evdref = ref Evd.empty in
@@ -544,16 +244,13 @@ let interp_mutual paramsl indl notations finite =
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
   let arities = List.map fst arities in
-  let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in
+  let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
     States.with_state_protection (fun () ->
      (* Temporary declaration of notations and scopes *)
-     List.iter (fun ((_,_,sc) as x ) ->
-       declare_interning_data impls x;
-       open_temp_scopes sc
-     ) notations;
+     List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      (* Interpret the constructor types *)
      list_map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl)
      () in
@@ -622,30 +319,25 @@ let extract_params indl =
 	"Parameters should be syntactically the same for each inductive type.";
       params
 
-let prepare_inductive ntnl indl =
-  let indl =
-    List.map (fun ((_,indname),_,ar,lc) -> {
-      ind_name = indname;
-      ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
-      ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
-    }) indl in
-  List.fold_right Option.List.cons ntnl [], indl
-
-
-let elim_flag = ref true
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optname  = "automatic declaration of eliminations";
-      optkey   = ["Elimination";"Schemes"];
-      optread  = (fun () -> !elim_flag) ;
-      optwrite = (fun b -> elim_flag := b) }
-
-let declare_mutual_with_eliminations isrecord mie impls =
+let extract_inductive indl =
+  List.map (fun ((_,indname),_,ar,lc) -> {
+    ind_name = indname;
+    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
+    ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
+  }) indl
+
+let extract_mutual_inductive_declaration_components indl =
+  let indl,ntnl = List.split indl in
+  let params = extract_params indl in
+  let coes = extract_coercions indl in
+  let indl = extract_inductive indl in
+  (params,indl), coes, List.fold_right Option.List.cons ntnl []
+
+let declare_mutual_inductive_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_,kn) = declare_mind isrecord mie in
-  let mind =Global.mind_of_delta (mind_of_kn kn) in
-    list_iter_i (fun i (indimpls, constrimpls) ->
+  let mind = Global.mind_of_delta (mind_of_kn kn) in
+  list_iter_i (fun i (indimpls, constrimpls) ->
 		   let ind = (mind,i) in
 		     Autoinstance.search_declaration (IndRef ind);
 		     maybe_declare_manual_implicits false (IndRef ind) indimpls;
@@ -655,54 +347,32 @@ let declare_mutual_with_eliminations isrecord mie impls =
 			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 		       constrimpls)
       impls;
-    if_verbose ppnl (minductive_message names);
-    if !elim_flag then declare_eliminations mind;
-    mind
+  if_verbose ppnl (minductive_message names);
+  declare_default_schemes mind;
+  mind
 
-let build_mutual l finite =
-  let indl,ntnl = List.split l in
-  let paramsl = extract_params indl in
-  let coes = extract_coercions indl in
-  let notations,indl = prepare_inductive ntnl indl in
-  let mie,impls = interp_mutual paramsl indl notations finite in
-  (* Declare the mutual inductive block with its eliminations *)
-  ignore (declare_mutual_with_eliminations false mie impls);
+open Vernacexpr
+
+type one_inductive_impls =
+  Impargs.manual_explicitation list (* for inds *)*
+  Impargs.manual_explicitation list list (* for constrs *)
+
+type one_inductive_expr =
+  lident * local_binder list * constr_expr option * constructor_expr list
+
+let do_mutual_inductive indl finite =
+  let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
+  (* Interpret the types *)
+  let mie,impls = interp_mutual_inductive indl ntns finite in
+  (* Declare the mutual inductive block with its associated schemes *)
+  ignore (declare_mutual_inductive_with_eliminations false mie impls);
   (* Declare the possible notations of inductive types *)
-  List.iter (declare_interning_data ([],[])) notations;
+  List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
   List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes
 
 (* 3c| Fixpoints and co-fixpoints *)
 
-let pr_rank = function
-  | 0 -> str "1st"
-  | 1 -> str "2nd"
-  | 2 -> str "3rd"
-  | n -> str ((string_of_int (n+1))^"th")
-
-let recursive_message indexes = function
-  | [] -> anomaly "no recursive definition"
-  | [id] -> pr_id id ++ str " is recursively defined" ++
-      (match indexes with
-	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
- 	 | _ -> mt ())
-  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
-		  spc () ++ str "are recursively defined" ++
-		  match indexes with
-		    | Some a -> spc () ++ str "(decreasing respectively on " ++
-			prlist_with_sep pr_coma pr_rank (Array.to_list a) ++
-			str " arguments)"
-		    | None -> mt ())
-
-let corecursive_message _ = function
-  | [] -> error "No corecursive definition."
-  | [id] -> pr_id id ++ str " is corecursively defined"
-  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
-                    spc () ++ str "are corecursively defined")
-
-let recursive_message isfix =
-  if isfix=Fixpoint then recursive_message else corecursive_message
-
 (* An (unoptimized) function that maps preorders to partial orders...
 
    Input:  a list of associations (x,[y1;...;yn]), all yi distincts
@@ -747,7 +417,7 @@ let rec partial_order = function
       in link y
     in browse (partial_order rest) [] xge
 
-let non_full_mutual_message x xge y yge kind rest =
+let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if List.mem x yge then
       string_of_id y^" depends on "^string_of_id x^" but not conversely"
@@ -756,13 +426,12 @@ let non_full_mutual_message x xge y yge kind rest =
     else
       string_of_id y^" and "^string_of_id x^" are not mutually dependent" in
   let e = if rest <> [] then "e.g.: "^reason else reason in
-  let k = if kind=Fixpoint then "fixpoint" else "cofixpoint" in
+  let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
-    if kind=Fixpoint then "Well-foundedness check may fail unexpectedly.\n"
-    else "" in
+    if isfix then "Well-foundedness check may fail unexpectedly.\n" else "" in
   "Not a fully mutually defined "^k^"\n("^e^").\n"^w
 
-let check_mutuality env kind fixl =
+let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
   let preorder =
     List.map (fun (id,def) ->
@@ -771,14 +440,10 @@ let check_mutuality env kind fixl =
   let po = partial_order preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
-	if_verbose warning (non_full_mutual_message x xge y yge kind rest)
+	if_verbose warning (non_full_mutual_message x xge y yge isfix rest)
     | _ -> ()
 
-type fixpoint_kind =
-  | IsFixpoint of (identifier located option * recursion_order_expr) list
-  | IsCoFixpoint
-
-type fixpoint_expr = {
+type structured_fixpoint_expr = {
   fix_name : identifier;
   fix_binders : local_binder list;
   fix_body : constr_expr;
@@ -826,7 +491,7 @@ let rec unfold f b =
     | Some (x, b') -> x :: unfold f b'
     | None -> []
 
-let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
+let compute_possible_guardness_evidences n fixctx fixtype =
   match n with
   | Some (loc, n) -> [rel_index n fixctx]
   | None ->
@@ -839,10 +504,11 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 	unfold (function x when x = len -> None
 	  | n -> Some (n, succ n)) 0
 
-let interp_recursive fixkind l boxed =
+type recursive_preentry =
+  identifier list * constr list * types list
+
+let interp_recursive isfix fixl notations =
   let env = Global.env() in
-  let fixl, ntnl = List.split l in
-  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -855,16 +521,12 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_types env fixnames fixtypes in
 
   (* Get interpretation metadatas *)
-  let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in
-  let notations = List.fold_right Option.List.cons ntnl [] in
+  let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
     States.with_state_protection (fun () ->
-      List.iter (fun ((_,_,sc) as x) ->
-        declare_interning_data impls x;
-        open_temp_scopes sc
-      ) notations;
+      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
 
@@ -875,410 +537,62 @@ let interp_recursive fixkind l boxed =
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
   List.iter (check_evars env_rec Evd.empty evd) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
-  check_mutuality env kind (List.combine fixnames fixdefs);
+  check_mutuality env isfix (List.combine fixnames fixdefs);
 
   (* Build the fix declaration block *)
   let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+  (snd (List.split fixctxs),fixnames,fixdecls,fixtypes),fiximps
+
+let interp_fixpoint fixl wfl notations =
+  let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
+    interp_recursive true fixl notations in
   let indexes, fixdecls =
-    match fixkind with
-    | IsFixpoint wfl ->
-	let possible_indexes =
-	  list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
-	let indexes = search_guard dummy_loc env possible_indexes fixdecls in
-	Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
-    | IsCoFixpoint ->
-	None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
+    let possible_indexes =
+      list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
+	let indexes =
+	  search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
+	Some indexes,
+	list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames
   in
+  ((fixnames,fixdecls,fixtypes),fiximps,indexes)
+
+let interp_cofixpoint fixl notations =
+  let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
+    interp_recursive false fixl notations in
+  let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+  ((fixnames,fixdecls,fixtypes),fiximps)
 
+let declare_fixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps,indexes) ntns =
+  ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
   (* Declare the recursive definitions *)
-  ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps);
-  if_verbose ppnl (recursive_message kind indexes fixnames);
+  fixpoint_message indexes fixnames;
+  (* Declare notations *)
+  List.iter Metasyntax.add_notation_interpretation ntns
 
+let declare_cofixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps) ntns =
+  ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
+  (* Declare the recursive definitions *)
+  cofixpoint_message fixnames;
   (* Declare notations *)
-  List.iter (declare_interning_data ([],[])) notations
-
-let build_recursive l b =
-  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
-  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
-    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
-    l in
-  interp_recursive (IsFixpoint g) fixl b
-
-let build_corecursive l b =
-  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
-    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
-    l in
-  interp_recursive IsCoFixpoint fixl b
-
-(* 3d| Schemes *)
-let rec split_scheme l =
- let env = Global.env() in
- match l with
-  | [] -> [],[]
-  | (Some id,t)::q -> let l1,l2 = split_scheme q in
-    ( match t with
-      | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2
-      | EqualityScheme  x -> l1,(x::l2)
-    )
-(*
- if no name has been provided, we build one from the types of the ind
-requested
-*)
-  | (None,t)::q ->
-       let l1,l2 = split_scheme q in
-    ( match t with
-      | InductionScheme (x,y,z) ->
-             let ind = smart_global_inductive y in
-             let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind)
-in
-             let z' = family_of_sort (interp_sort z) in
-             let suffix = (
-                match sort_of_ind with
-                | InProp ->
-                    if x then (match z' with
-                       | InProp -> "_ind_nodep"
-                       | InSet -> "_rec_nodep"
-                       | InType -> "_rect_nodep")
-                    else ( match z' with
-                       | InProp -> "_ind"
-                       | InSet -> "_rec"
-                       | InType -> "_rect" )
-                | _ ->
-                    if x then (match z' with
-                       | InProp -> "_ind"
-                       | InSet -> "_rec"
-                       | InType -> "_rect" )
-                    else (match z' with
-                       | InProp -> "_ind_nodep"
-                       | InSet  -> "_rec_nodep"
-                       | InType -> "_rect_nodep")
-                ) in
-            let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
-            let newref = (dummy_loc,newid) in
-          ((newref,x,y,z)::l1),l2
-      | EqualityScheme  x -> l1,(x::l2)
-    )
-
-
-let build_induction_scheme lnamedepindsort =
-  let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
-  and sigma = Evd.empty
-  and env0 = Global.env() in
-  let lrecspec =
-    List.map
-      (fun (_,dep,indid,sort) ->
-        let ind = smart_global_inductive indid in
-        let (mib,mip) = Global.lookup_inductive ind in
-         (ind,mib,mip,dep,interp_elimination_sort sort))
-      lnamedepindsort
-  in
-  let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in
-  let rec declare decl fi lrecref =
-    let decltype = Retyping.get_type_of env0 Evd.empty decl in
-    let decltype = refresh_universes decltype in
-    let ce = { const_entry_body = decl;
-               const_entry_type = Some decltype;
-               const_entry_opaque = false;
-	       const_entry_boxed = Flags.boxed_definitions() } in
-    let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in
-    ConstRef kn :: lrecref
-  in
-  let _ = List.fold_right2 declare listdecl lrecnames [] in
-  if_verbose ppnl (recursive_message Fixpoint None lrecnames)
-
-let build_scheme l =
-  let ischeme,escheme = split_scheme l in
-(* we want 1 kind of scheme at a time so we check if the user
-tried to declare different schemes at once *)
-    if (ischeme <> []) && (escheme <> [])
-    then
-      error "Do not declare equality and induction scheme at the same time."
-    else (
-      if ischeme <> [] then build_induction_scheme ischeme;
-      List.iter ( fun indname ->
-        let ind = smart_global_inductive indname
-        in declare_eq_scheme (fst ind);
-        try
-           make_eq_decidability ind
-        with _ ->
-          Pfedit.delete_current_proof();
-          message "Error while computing decidability scheme. Please report."
-      ) escheme
-    )
-
-let list_split_rev_at index l =
-  let rec aux i acc = function
-      hd :: tl when i = index -> acc, tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_when: Invalid argument"
-  in aux 0 [] l
-
-let fold_left' f = function
-    [] -> raise (Invalid_argument "fold_right'")
-  | hd :: tl -> List.fold_left f hd tl
-
-let build_combined_scheme name schemes =
-  let env = Global.env () in
-(*   let nschemes = List.length schemes in *)
-  let find_inductive ty =
-    let (ctx, arity) = decompose_prod ty in
-    let (_, last) = List.hd ctx in
-      match kind_of_term last with
-	| App (ind, args) ->
-	    let ind = destInd ind in
-	    let (_,spec) = Inductive.lookup_mind_specif env ind in
-	      ctx, ind, spec.mind_nrealargs
-	| _ -> ctx, destInd last, 0
-  in
-  let defs =
-    List.map (fun x ->
-		let refe = Ident x in
-		let qualid = qualid_of_reference refe in
-		let cst = try Nametab.locate_constant (snd qualid)
-                  with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
-                in
-		let ty = Typeops.type_of_constant env cst in
-		  qualid, cst, ty)
-      schemes
-  in
-  let (qid, c, t) = List.hd defs in
-  let ctx, ind, nargs = find_inductive t in
-  (* Number of clauses, including the predicates quantification *)
-  let prods = nb_prod t - (nargs + 1) in
-  let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
-  let relargs = rel_vect 0 prods in
-  let concls = List.rev_map
-    (fun (_, cst, t) ->
-      mkApp(mkConst cst, relargs),
-      snd (decompose_prod_n prods t)) defs in
-  let concl_bod, concl_typ =
-    fold_left'
-      (fun (accb, acct) (cst, x) ->
-	mkApp (coqconj, [| x; acct; cst; accb |]),
-	mkApp (coqand, [| x; acct |])) concls
-  in
-  let ctx, _ =
-    list_split_rev_at prods
-      (List.rev_map (fun (x, y) -> x, None, y) ctx) in
-  let typ = it_mkProd_wo_LetIn concl_typ ctx in
-  let body = it_mkLambda_or_LetIn concl_bod ctx in
-  let ce = { const_entry_body = body;
-             const_entry_type = Some typ;
-             const_entry_opaque = false;
-	     const_entry_boxed = Flags.boxed_definitions() } in
-  let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in
-    if_verbose ppnl (recursive_message Fixpoint None [snd name])
-(* 4| Goal declaration *)
-
-(* 4.1| Support for mutually proved theorems *)
-
-let retrieve_first_recthm = function
-  | VarRef id ->
-      (pi2 (Global.lookup_named id),variable_opacity id)
-  | ConstRef cst ->
-      let {const_body=body;const_opaque=opaq} =	Global.lookup_constant cst in
-      (Option.map Declarations.force body,opaq)
-  | _ -> assert false
-
-let default_thm_id = id_of_string "Unnamed_thm"
-
-let compute_proof_name = function
-  | Some (loc,id) ->
-      (* We check existence here: it's a bit late at Qed time *)
-      if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-        user_err_loc (loc,"",pr_id id ++ str " already exists.");
-      id
-  | None ->
-      let rec next avoid id =
-        let id = next_global_ident_away false id avoid in
-        if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id
-        else id
-      in
-      next (Pfedit.get_all_proof_names ()) default_thm_id
-
-let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
-  match body with
-  | None ->
-      (match local with
-      | Local ->
-          let impl=false in (* copy values from Vernacentries *)
-          let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum (t_i,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (Local,VarRef id,imps)
-      | Global ->
-          let k = IsAssumption Conjectural in
-          let kn = declare_constant id (ParameterEntry (t_i,false), k) in
-          (Global,ConstRef kn,imps))
-  | Some body ->
-      let k = logical_kind_of_goal_kind kind in
-      let body_i = match kind_of_term body with
-        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-        | CoFix (0,decls) -> mkCoFix (i,decls)
-        | _ -> anomaly "Not a proof by induction" in
-      match local with
-      | Local ->
-	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
-	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Local,VarRef id,imps)
-      | Global ->
-          let const =
-            { const_entry_body = body_i;
-              const_entry_type = Some t_i;
-              const_entry_opaque = opaq;
-              const_entry_boxed = false (* copy of what cook_proof does *)} in
-          let kn = declare_constant id (DefinitionEntry const, k) in
-          (Global,ConstRef kn,imps)
-
-let look_for_mutual_statements thms =
-  if List.tl thms <> [] then
-    (* More than one statement: we look for a common inductive hyp or a *)
-    (* common coinductive conclusion *)
-    let n = List.length thms in
-    let inds = List.map (fun (id,(t,_) as x) ->
-      let (hyps,ccl) = decompose_prod_assum t in
-      let whnf_hyp_hds = map_rel_context_in_env
-        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
-        (Global.env()) hyps in
-      let ind_hyps =
-        List.flatten (list_map_i (fun i (_,b,t) ->
-          match kind_of_term t with
-          | Ind (kn,_ as ind) when
-                let mind = Global.lookup_mind kn in
-                mind.mind_finite & b = None ->
-              [ind,x,i]
-          | _ ->
-              []) 1 (List.rev whnf_hyp_hds)) in
-      let ind_ccl =
-        let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
-        match kind_of_term whnf_ccl with
-        | Ind (kn,_ as ind) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_ntypes = n & not mind.mind_finite ->
-            [ind,x,0]
-        | _ ->
-            [] in
-      ind_hyps,ind_ccl) thms in
-    let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
-    (* Check if all conclusions are coinductive in the same type *)
-    (* (degenerated cartesian product since there is at most one coind ccl) *)
-    let same_indccl =
-      list_cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] ind_ccls in
-    let ordered_same_indccl =
-      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
-    (* Check if some hypotheses are inductive in the same type *)
-    let common_same_indhyp =
-      list_cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] inds_hyps in
-    let ordered_inds,finite =
-      match ordered_same_indccl, common_same_indhyp with
-      | indccl::rest, _ ->
-	  assert (rest=[]);
-          (* One occ. of common coind ccls and no common inductive hyps *)
-	  if common_same_indhyp <> [] then
-	    if_verbose warning "Assuming mutual coinductive statements.";
-	  flush_all ();
-          indccl, true
-      | [], _::_ ->
-	  if same_indccl <> [] &&
-	     list_distinct (List.map pi1 (List.hd same_indccl)) then
-	    if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
-	  (* assume the largest indices as possible *)
-	  list_last common_same_indhyp, false
-      | _, [] ->
-	  error
-            ("Cannot find common (mutual) inductive premises or coinductive" ^
-             " conclusions in the statements.")
-    in
-    let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
-    let rec_tac =
-      if finite then
-        match List.map (fun (id,(t,_)) -> (id,t)) thms with
-        | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
-        | _ -> assert false
-      else
-	(* nl is dummy: it will be recomputed at Qed-time *)
-        match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
-        | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
-        | _ -> assert false in
-    Some rec_tac,thms
-  else
-    None, thms
-
-(* 4.2| General support for goals *)
-
-let start_proof_com kind thms hook =
-  let evdref = ref (create_evar_defs Evd.empty) in
-  let env = Global.env () in
-  let thms = List.map (fun (sopt,(bl,t)) ->
-    let (env, ctx), imps = interp_context_evars evdref env bl in
-    let t', imps' = interp_type_evars_impls ~evdref env t in
-    let len = List.length ctx in
-      (compute_proof_name sopt,
-      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'))))
-    thms in
-  let rec_tac,thms = look_for_mutual_statements thms in
-  match thms with
-  | [] -> anomaly "No proof to start"
-  | (id,(t,(len,imps)) as thm)::other_thms ->
-      let hook strength ref =
-        let other_thms_data =
-          if other_thms = [] then [] else
-            (* there are several theorems defined mutually *)
-            let body,opaq = retrieve_first_recthm ref in
-            list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
-        let thms_data = (strength,ref,imps)::other_thms_data in
-        List.iter (fun (strength,ref,imps) ->
-	  maybe_declare_manual_implicits false ref imps;
-	  hook strength ref) thms_data in
-      let init_tac =
-	let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
-	  if Flags.is_auto_intros () then
-	    match rec_tac with
- 	    | None -> Some (intro_tac thm)
-	    | Some tac -> Some (Tacticals.tclTHENS tac (List.map intro_tac thms))
-	  else rec_tac
-      in start_proof id kind t ?init_tac hook ~compute_guard:(rec_tac<>None)
-
-let check_anonymity id save_ident =
-  if atompart_of_id id <> "Unnamed_thm" then
-    error "This command can only be used for unnamed theorem."
-(*
-    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
-*)
+  List.iter Metasyntax.add_notation_interpretation ntns
 
-let save_anonymous opacity save_ident =
-  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  save save_ident const do_guard persistence hook
-
-let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
-  let const = { const with const_entry_opaque = opacity } in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const do_guard (Global, Proof kind) hook
-
-let admit () =
-  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
-(* Contraire aux besoins d'interactivité...
-  if k <> IsGlobal (Proof Conjecture) then
-    error "Only statements declared as conjecture can be admitted";
-*)
-  let kn =
-    declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in
-  Pfedit.delete_current_proof ();
-  assumption_message id;
-  hook Global (ConstRef kn)
+let extract_fixpoint_components l =
+  let fixl, ntnl = List.split l in
+  let wfl = List.map (fun (_,wf,_,_,_) -> fst wf) fixl in
+  let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
+    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+  fixl, List.fold_right Option.List.cons ntnl [], wfl
+
+let extract_cofixpoint_components l =
+  let fixl, ntnl = List.split l in
+  List.map (fun ((_,id),bl,typ,def) ->
+    {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+  List.fold_right Option.List.cons ntnl []
 
-let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+let do_fixpoint l b =
+  let fixl,ntns,wfl = extract_fixpoint_components l in
+  declare_fixpoint b (interp_fixpoint fixl wfl ntns) ntns
 
+let do_cofixpoint l b =
+  let fixl,ntns = extract_cofixpoint_components l in
+  declare_cofixpoint b (interp_cofixpoint fixl ntns) ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 14cfef6b2..05ee67d79 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -12,139 +12,146 @@
 open Util
 open Names
 open Term
-open Nametab
-open Declare
-open Library
+open Entries
 open Libnames
-open Nametab
 open Tacexpr
 open Vernacexpr
-open Rawterm
 open Topconstr
 open Decl_kinds
 open Redexpr
+open Constrintern
 (*i*)
 
-(*s Declaration functions. The following functions take ASTs,
-   transform them into [constr] and then call the corresponding
-   functions of [Declare]; they return an absolute reference to the
-   defined object *)
+(*s This file is about the interpretation of raw commands into typed
+    ones and top-level declaration of the main Gallina objects *)
 
-val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit)
-val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
+(* Hooks for Pcoq *)
 
-val definition_message : identifier -> unit
-val assumption_message : identifier -> unit
+val set_declare_definition_hook : (definition_entry -> unit) -> unit
+val get_declare_definition_hook : unit -> (definition_entry -> unit)
+val set_declare_assumptions_hook : (types -> unit) -> unit
 
-val declare_definition : identifier -> definition_kind ->
-  local_binder list -> red_expr option -> constr_expr ->
-  constr_expr option -> declaration_hook -> unit
+(*************************************************************************)
+(* Definitions/Let *)
 
-val syntax_definition : identifier -> identifier list * constr_expr ->
-  bool -> bool -> unit
+val interp_definition :
+  boxed_flag -> local_binder list -> red_expr option -> constr_expr ->
+  constr_expr option -> definition_entry * manual_implicits
 
-val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
-  Impargs.manual_explicitation list ->
-  bool (* implicit *) -> bool (* inline *) -> Names.variable located  -> unit
+val declare_definition : identifier -> locality * definition_object_kind ->
+  definition_entry -> manual_implicits -> declaration_hook -> unit
 
-val set_declare_assumption_hook : (types -> unit) -> unit
+(*************************************************************************)
+(* Parameters/Assumptions *)
 
-val declare_assumption : identifier located list ->
-  coercion_flag -> assumption_kind -> local_binder list -> constr_expr ->
-  bool -> bool -> unit
+val interp_assumption :
+  local_binder list -> constr_expr -> types * manual_implicits
 
-val open_temp_scopes : Topconstr.scope_name option -> unit
+val declare_assumption : coercion_flag -> assumption_kind -> types ->
+  manual_implicits ->
+  bool (* implicit *) -> bool (* inline *) -> variable located -> unit
 
-val declare_interning_data : 'a * Constrintern.implicits_env ->
-    string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
+val declare_assumptions : variable located list ->
+  coercion_flag -> assumption_kind -> types -> manual_implicits ->
+  bool -> bool -> unit
 
-val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type ->
-  'a list -> 'b list ->
-  Term.types list ->Impargs.manual_explicitation list list ->
-  'a list *
-    ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list *
-	      Topconstr.scope_name option list))
-    list
+(*************************************************************************)
+(* Inductive and coinductive types *)
 
-val check_mutuality : Environ.env -> definition_object_kind ->
-  (identifier * types) list -> unit
+(* Extracting the semantical components out of the raw syntax of mutual
+   inductive declarations *)
 
-val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) *
-		                decl_notation) list -> bool -> unit
+type structured_one_inductive_expr = {
+  ind_name : identifier;
+  ind_arity : constr_expr;
+  ind_lc : (identifier * constr_expr) list
+}
 
-val declare_mutual_with_eliminations :
-  bool -> Entries.mutual_inductive_entry ->
-  (Impargs.manual_explicitation list *
-      Impargs.manual_explicitation list list) list ->
-  mutual_inductive
+type structured_inductive_expr =
+  local_binder list * structured_one_inductive_expr list
 
-type fixpoint_kind =
-  | IsFixpoint of (identifier located option * recursion_order_expr) list
-  | IsCoFixpoint
+val extract_mutual_inductive_declaration_components :
+  (one_inductive_expr * decl_notation option) list ->
+    structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
 
-type fixpoint_expr = {
-  fix_name : identifier;
-  fix_binders : local_binder list;
-  fix_body : constr_expr;
-  fix_type : constr_expr
-}
+(* Typing mutual inductive definitions *)
 
-val recursive_message : definition_object_kind ->
-  int array option -> identifier list -> Pp.std_ppcmds
+type one_inductive_impls =
+  Impargs.manual_explicitation list (* for inds *)*
+  Impargs.manual_explicitation list list (* for constrs *)
 
-val declare_fix : bool -> definition_object_kind -> identifier ->
-  constr -> types -> Impargs.manual_explicitation list -> global_reference
+val interp_mutual_inductive :
+  structured_inductive_expr -> decl_notation list -> bool ->
+    mutual_inductive_entry * one_inductive_impls list
 
-val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
+(* Registering a mutual inductive definition together with its
+   associated schemes *)
 
-val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit
+val declare_mutual_inductive_with_eliminations :
+  bool -> mutual_inductive_entry -> one_inductive_impls list ->
+  mutual_inductive
 
-val build_scheme : (identifier located option * scheme ) list -> unit
+(* Entry points for the vernacular commands Inductive and CoInductive *)
 
-val build_combined_scheme : identifier located -> identifier located list -> unit
+val do_mutual_inductive :
+  (one_inductive_expr * decl_notation option) list -> bool -> unit
 
-val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
+(*************************************************************************)
+(* Fixpoints and cofixpoints *)
 
-val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+type structured_fixpoint_expr = {
+  fix_name : identifier;
+  fix_binders : local_binder list;
+  fix_body : constr_expr;
+  fix_type : constr_expr
+}
 
-(* A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
+(* Extracting the semantical components out of the raw syntax of
+   (co)fixpoints declarations *)
 
-val start_proof : identifier -> goal_kind -> types ->
-  ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
+val extract_fixpoint_components :
+  (fixpoint_expr * decl_notation option) list ->
+    structured_fixpoint_expr list * decl_notation list *
+    (* possible structural arg: *) lident option list
 
-val start_proof_com : goal_kind ->
-  (lident option * (local_binder list * constr_expr)) list ->
-  declaration_hook -> unit
+val extract_cofixpoint_components :
+  (cofixpoint_expr * decl_notation option) list ->
+    structured_fixpoint_expr list * decl_notation list
 
-(* A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Refiner.pftreestate -> unit) -> unit
+(* Typing fixpoints and cofixpoint_expr *)
 
-(*s [save_named b] saves the current completed proof under the name it
-was started; boolean [b] tells if the theorem is declared opaque; it
-fails if the proof is not completed *)
+type recursive_preentry =
+  identifier list * constr list * types list
 
-val save_named : bool -> unit
+val interp_fixpoint :
+  structured_fixpoint_expr list -> lident option list -> decl_notation list ->
+    recursive_preentry * manual_implicits list * int array option
 
-(* [save_anonymous b name] behaves as [save_named] but declares the theorem
-under the name [name] and respects the strength of the declaration *)
+val interp_cofixpoint :
+  structured_fixpoint_expr list -> decl_notation list ->
+    recursive_preentry * manual_implicits list
 
-val save_anonymous : bool -> identifier -> unit
+(* Registering fixpoints and cofixpoints in the environment *)
 
-(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
-   declares the theorem under the name [name] and gives it the
-   strength [strength] *)
+val declare_fixpoint :
+  bool -> recursive_preentry * manual_implicits list * int array option ->
+    decl_notation list -> unit
 
-val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
+val declare_cofixpoint :
+  bool -> recursive_preentry * manual_implicits list ->
+    decl_notation list -> unit
 
-(* [admit ()] aborts the current goal and save it as an assmumption *)
+(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
-val admit : unit -> unit
+val do_fixpoint :
+  (fixpoint_expr * decl_notation option) list -> bool -> unit
 
-(* [get_current_context ()] returns the evar context and env of the
-   current open proof if any, otherwise returns the empty evar context
-   and the current global env *)
+val do_cofixpoint :
+  (cofixpoint_expr * decl_notation option) list -> bool -> unit
 
-val get_current_context : unit -> Evd.evar_map * Environ.env
+(* Utils *)
 
+val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit
 
+val declare_fix : bool -> definition_object_kind -> identifier ->
+  constr -> types -> Impargs.manual_explicitation list -> global_reference
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 245f96227..447aeca48 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -8,75 +8,163 @@
 
 (*i $Id$ i*)
 
-open Names
-open Mod_subst
-
-let eq_scheme_map = ref Indmap.empty
-
-let cache_scheme (_,(ind,const)) =
-    eq_scheme_map := Indmap.add ind const (!eq_scheme_map)
-
-
-
-let _ = Summary.declare_summary "eqscheme"
-    { Summary.freeze_function = (fun () -> !eq_scheme_map);
-      Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs);
-      Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty) }
-
-let find_eq_scheme ind =
-  Indmap.find ind !eq_scheme_map
-
-let check_eq_scheme ind =
-  Indmap.mem ind !eq_scheme_map
-
-let bl_map = ref Indmap.empty
-let lb_map = ref Indmap.empty
-let dec_map = ref Indmap.empty
-
-
-let cache_bl (_,(ind,const)) =
-    bl_map := Indmap.add ind const (!bl_map)
-
-let cache_lb (_,(ind,const)) =
-    lb_map := Indmap.add ind const (!lb_map)
-
-let cache_dec (_,(ind,const)) =
-    dec_map := Indmap.add ind const (!dec_map)
-
-
-
-let _ = Summary.declare_summary "bl_proof"
-    { Summary.freeze_function = (fun () -> !bl_map);
-      Summary.unfreeze_function = (fun fs -> bl_map := fs);
-      Summary.init_function = (fun () -> bl_map := Indmap.empty) }
-
-let find_bl_proof ind =
-  Indmap.find ind !bl_map
-
-let check_bl_proof ind =
-  Indmap.mem ind !bl_map
-
-let _ = Summary.declare_summary "lb_proof"
-    { Summary.freeze_function = (fun () -> !lb_map);
-      Summary.unfreeze_function = (fun fs -> lb_map := fs);
-      Summary.init_function = (fun () -> lb_map := Indmap.empty) }
-
-let find_lb_proof ind =
-  Indmap.find ind !lb_map
-
-let check_lb_proof ind =
-  Indmap.mem ind !lb_map
-
-let _ = Summary.declare_summary "eq_dec_proof"
-    { Summary.freeze_function = (fun () -> !dec_map);
-      Summary.unfreeze_function = (fun fs -> dec_map := fs);
-      Summary.init_function = (fun () -> dec_map := Indmap.empty) }
-
-let find_eq_dec_proof ind =
-  Indmap.find ind !dec_map
-
-let check_dec_proof ind =
-  Indmap.mem ind !dec_map
+(* File created by Vincent Siles, Oct 2007, extended into a generic
+   support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
 
+(* This file provides support for registering inductive scheme builders,
+   declaring schemes and generating schemes on demand *)
 
+open Names
+open Mod_subst
+open Libobject
+open Nameops
+open Declarations
+open Term
+open Util
+open Declare
+open Entries
+open Decl_kinds
+
+(**********************************************************************)
+(* Registering schemes in the environment *)
+
+type mutual_scheme_object_function = mutual_inductive -> constr array
+type individual_scheme_object_function = inductive -> constr
+
+type 'a scheme_kind = string
+
+let scheme_map = ref Indmap.empty
+
+let cache_one_scheme kind (ind,const) =
+  let map = try Indmap.find ind !scheme_map with Not_found -> Stringmap.empty in
+  scheme_map := Indmap.add ind (Stringmap.add kind const map) !scheme_map
+
+let cache_scheme (_,(kind,l)) =
+  Array.iter (cache_one_scheme kind) l
+
+let subst_one_scheme subst ((mind,i),const) =
+  (* Remark: const is a def: the result of substitution is a constant *)
+  ((subst_ind subst mind,i),fst (subst_con subst const))
+
+let subst_scheme (subst,(kind,l)) =
+  (kind,Array.map (subst_one_scheme subst) l)
+
+let discharge_scheme (_,(kind,l)) =
+  Some (kind,Array.map (fun (ind,const) ->
+    (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
+
+let (inScheme,_) =
+  declare_object {(default_object "SCHEME") with
+                    cache_function = cache_scheme;
+                    load_function = (fun _ -> cache_scheme);
+                    subst_function = subst_scheme;
+		    classify_function = (fun obj -> Substitute obj);
+		    discharge_function = discharge_scheme}
+
+(**********************************************************************)
+(* Saving/restoring the table of scheme *)
+
+let freeze_schemes () = !scheme_map
+let unfreeze_schemes sch = scheme_map := sch
+let init_schemes () = scheme_map := Indmap.empty
+
+let _ =
+  Summary.declare_summary "Schemes"
+    { Summary.freeze_function = freeze_schemes;
+      Summary.unfreeze_function = unfreeze_schemes;
+      Summary.init_function = init_schemes }
+
+(**********************************************************************)
+(* The table of scheme building functions *)
+
+type individual
+type mutual
+
+type scheme_object_function =
+  | MutualSchemeFunction of (mutual_inductive -> constr array)
+  | IndividualSchemeFunction of (inductive -> constr)
+
+let scheme_object_table =
+  (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
+
+let declare_scheme_object s aux f =
+  (try check_ident ("ind"^s) with _ ->
+    error ("Illegal induction scheme suffix: "^s));
+  let key = if aux = "" then s else aux in
+  try
+    let _ = Hashtbl.find scheme_object_table key in
+(*    let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
+    error ("Scheme object "^key^" already declared.")
+  with Not_found ->
+    Hashtbl.add scheme_object_table key (s,f);
+    key
+
+let declare_mutual_scheme_object s ?(aux="") f =
+  declare_scheme_object s aux (MutualSchemeFunction f)
+
+let declare_individual_scheme_object s ?(aux="") f =
+  declare_scheme_object s aux (IndividualSchemeFunction f)
+
+(**********************************************************************)
+(* Defining/retrieving schemes *)
+
+let declare_scheme kind indcl =
+  Lib.add_anonymous_leaf (inScheme (kind,indcl))
+
+let define internal id c =
+  let fd = if internal then declare_internal_constant else declare_constant in
+  let kn = fd id
+    (DefinitionEntry
+      { const_entry_body = c;
+        const_entry_type = None;
+        const_entry_opaque = false;
+	const_entry_boxed = Flags.boxed_definitions() },
+      Decl_kinds.IsDefinition Scheme) in
+  definition_message id;
+  kn
+
+let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
+  let c = f ind in
+  let mib = Global.lookup_mind mind in
+  let id = match idopt with
+    | Some id -> id
+    | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
+  let const = define internal id c in
+  declare_scheme kind [|ind,const|];
+  const
+
+let define_individual_scheme kind internal names (mind,i as ind) =
+  match Hashtbl.find scheme_object_table kind with
+  | _,MutualSchemeFunction f -> assert false
+  | s,IndividualSchemeFunction f ->
+      define_individual_scheme_base kind s f internal names ind
+
+let define_mutual_scheme_base kind suff f internal names mind =
+  let cl = f mind in
+  let mib = Global.lookup_mind mind in
+  let ids = Array.init (Array.length mib.mind_packets) (fun i ->
+      try List.assoc i names
+      with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
+  let consts = array_map2 (define internal) ids cl in
+  declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
+  consts
+
+let define_mutual_scheme kind internal names mind =
+  match Hashtbl.find scheme_object_table kind with
+  | _,IndividualSchemeFunction _ -> assert false
+  | s,MutualSchemeFunction f ->
+      define_mutual_scheme_base kind s f internal names mind
+
+let find_scheme kind (mind,i as ind) =
+  try Stringmap.find kind (Indmap.find ind !scheme_map)
+  with Not_found ->
+  match Hashtbl.find scheme_object_table kind with
+  | s,IndividualSchemeFunction f ->
+      define_individual_scheme_base kind s f true None ind
+  | s,MutualSchemeFunction f ->
+      (define_mutual_scheme_base kind s f true [] mind).(i)
+
+let check_scheme kind ind =
+  try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
+  with Not_found -> false
 
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index e13eedbdc..57ebbcda1 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -11,25 +11,41 @@ open Names
 open Libnames
 open Mod_subst
 open Sign
+open Declarations
 
+(* This module provides support for registering inductive scheme builders,
+   declaring schemes and generating schemes on demand *)
 
-val cache_scheme :(object_name*(Indmap.key*constr)) -> unit
+(* A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
 
-val find_eq_scheme : Indmap.key -> constr
-val check_eq_scheme : Indmap.key -> bool
+type mutual
+type individual
+type 'a scheme_kind
 
-val cache_bl: (object_name*(Indmap.key*constr)) -> unit
-val cache_lb: (object_name*(Indmap.key*constr)) -> unit
-val cache_dec : (object_name*(Indmap.key*constr)) -> unit
+type mutual_scheme_object_function = mutual_inductive -> constr array
+type individual_scheme_object_function = inductive -> constr
 
-val find_bl_proof : Indmap.key -> constr
-val find_lb_proof : Indmap.key -> constr
-val find_eq_dec_proof : Indmap.key -> constr
+(* Main functions to register a scheme builder *)
 
-val check_bl_proof: Indmap.key -> bool
-val check_lb_proof: Indmap.key -> bool
-val check_dec_proof: Indmap.key -> bool
+val declare_mutual_scheme_object : string -> ?aux:string ->
+  mutual_scheme_object_function -> mutual scheme_kind
 
+val declare_individual_scheme_object : string -> ?aux:string ->
+  individual_scheme_object_function -> individual scheme_kind
 
+(*
+val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
+*)
 
+(* Force generation of a (mutually) scheme with possibly user-level names *)
 
+val define_individual_scheme : individual scheme_kind -> bool (* internal *) ->
+  identifier option -> inductive -> constant
+
+val define_mutual_scheme : mutual scheme_kind -> bool (* internal *) ->
+  (int * identifier) list -> mutual_inductive -> constant array
+
+(* Main function to retrieve a scheme in the cache or to generate it *)
+val find_scheme : 'a scheme_kind -> inductive -> constant
+
+val check_scheme : 'a scheme_kind -> inductive -> bool
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
new file mode 100644
index 000000000..9f05c3e6c
--- /dev/null
+++ b/toplevel/indschemes.ml
@@ -0,0 +1,536 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* Created by Hugo Herbelin from contents related to inductive schemes
+   initially developed by Christine Paulin (induction schemes), Vincent
+   Siles (decidable equality and boolean equality) and Matthieu Sozeau
+   (combined scheme) in file command.ml, Sep 2009 *)
+
+(* This file provides entry points for manually or automatically
+   declaring new schemes *)
+
+open Pp
+open Flags
+open Util
+open Names
+open Declarations
+open Entries
+open Term
+open Inductive
+open Decl_kinds
+open Indrec
+open Declare
+open Libnames
+open Goptions
+open Nameops
+open Termops
+open Typeops
+open Inductiveops
+open Pretyping
+open Topconstr
+open Nametab
+open Smartlocate
+open Vernacexpr
+open Ind_tables
+open Auto_ind_decl
+open Eqschemes
+
+(* Flags governing automatic synthesis of schemes *)
+
+let elim_flag = ref true
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic declaration of induction schemes";
+      optkey   = ["Elimination";"Schemes"];
+      optread  = (fun () -> !elim_flag) ;
+      optwrite = (fun b -> elim_flag := b) }
+
+let case_flag = ref true
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic declaration of case analysis schemes";
+      optkey   = ["Case";"Analysis";"Schemes"];
+      optread  = (fun () -> !elim_flag) ;
+      optwrite = (fun b -> elim_flag := b) }
+
+let eq_flag = ref true
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic declaration of boolean equality";
+      optkey   = ["Boolean";"Equality";"Schemes"];
+      optread  = (fun () -> !eq_flag) ;
+      optwrite = (fun b -> eq_flag := b) }
+let _ = (* compatibility *)
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic declaration of boolean equality";
+      optkey   = ["Equality";"Scheme"];
+      optread  = (fun () -> !eq_flag) ;
+      optwrite = (fun b -> eq_flag := b) }
+
+let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+
+let eq_dec_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic declaration of decidable equality";
+      optkey   = ["Decidable";"Equality";"Schemes"];
+      optread  = (fun () -> !eq_dec_flag) ;
+      optwrite = (fun b -> eq_dec_flag := b) }
+
+let rewriting_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  ="automatic declaration of rewriting schemes for equality types";
+      optkey   = ["Rewriting";"Schemes"];
+      optread  = (fun () -> !rewriting_flag) ;
+      optwrite = (fun b -> rewriting_flag := b) }
+
+(* Util *)
+
+let define id internal c t =
+  let f = if internal then declare_internal_constant else declare_constant in
+  let kn = f id
+    (DefinitionEntry
+      { const_entry_body = c;
+        const_entry_type = t;
+        const_entry_opaque = false;
+	const_entry_boxed = Flags.boxed_definitions() },
+      Decl_kinds.IsDefinition Scheme) in
+  definition_message id;
+  kn
+
+(* Boolean equality *)
+
+let declare_beq_scheme_gen internal names kn =
+  ignore (define_mutual_scheme beq_scheme_kind internal names kn)
+
+let alarm what internal msg =
+  let debug = false in
+  if internal then
+    (if debug then
+      Flags.if_verbose Pp.msg_warning
+	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
+  else
+    errorlabstrm "" msg
+
+let try_declare_scheme what f internal names kn =
+  try f internal names kn
+  with
+    | ParameterWithoutEquality cst ->
+	alarm what internal
+	  (str "Boolean equality not found for parameter " ++ pr_con cst ++
+	   str".")
+    | InductiveWithProduct ->
+	alarm what internal
+	  (str "Unable to decide equality of functional arguments.")
+    | InductiveWithSort ->
+	alarm what internal
+	  (str "Unable to decide equality of type arguments.")
+    | NonSingletonProp ind ->
+	alarm what internal
+	  (str "Cannot extract computational content from proposition " ++
+	   quote (Printer.pr_inductive (Global.env()) ind) ++ str ".")
+    | EqNotFound (ind',ind) ->
+	alarm what internal
+	  (str "Boolean equality on " ++
+	   quote (Printer.pr_inductive (Global.env()) ind') ++
+	   strbrk " is missing.")
+    | UndefinedCst s ->
+	alarm what internal
+	  (strbrk "Required constant " ++ str s ++ str " undefined.")
+    | _ ->
+	alarm what internal
+	  (str "Unknown exception during scheme creation.")
+
+let beq_scheme_msg mind =
+  let mib = Global.lookup_mind mind in
+  (* TODO: mutual inductive case *)
+  str "Boolean equality on " ++
+    pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind))
+    (list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
+
+let declare_beq_scheme_with l kn =
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen false l kn
+
+let try_declare_beq_scheme kn =
+  (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
+      proof-irrelevance; improve decidability by depending on decidability
+      for the parameters rather than on the bl and lb properties *)
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen true [] kn
+
+let declare_beq_scheme = declare_beq_scheme_with []
+
+(* Induction/recursion schemes *)
+
+let optimize_non_type_induction_scheme kind dep sort ind =
+  if check_scheme kind ind then
+    (* in case the inductive has a type elimination, generates only one
+       induction scheme, the other ones share the same code with the
+       apropriate type *)
+    let cte = find_scheme kind ind in
+    let c = mkConst cte in
+    let t = type_of_constant (Global.env()) cte in
+    let (mib,mip) = Global.lookup_inductive ind in
+    let npars =
+      (* if a constructor of [ind] contains a recursive call, the scheme
+	 is generalized only wrt recursively uniform parameters *)
+      if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs)
+      then
+	mib.mind_nparams_rec
+      else
+	mib.mind_nparams in
+    snd (weaken_sort_scheme (new_sort_in_family sort) npars c t)
+  else
+    build_induction_scheme (Global.env()) Evd.empty ind dep InProp
+
+let build_induction_scheme_in_type dep sort ind =
+  build_induction_scheme (Global.env()) Evd.empty ind dep sort
+
+let rect_scheme_kind_from_type =
+  declare_individual_scheme_object "_rect_nodep"
+    (build_induction_scheme_in_type false InType)
+
+let rect_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
+    (build_induction_scheme_in_type false InType)
+
+let rect_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
+    (build_induction_scheme_in_type true InType)
+
+let rect_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rect_dep"
+    (build_induction_scheme_in_type true InType)
+
+let ind_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind_nodep"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
+
+let ind_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
+
+let ind_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
+
+let ind_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind_dep"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp)
+
+let rec_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec_nodep"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
+
+let rec_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
+
+let rec_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
+
+let rec_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_rec_dep"
+  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet)
+
+let kinds_from_prop =
+  [InType,rect_scheme_kind_from_prop;
+   InProp,ind_scheme_kind_from_prop;
+   InSet,rec_scheme_kind_from_prop]
+
+let kinds_from_type =
+  [InType,rect_dep_scheme_kind_from_type;
+   InProp,ind_dep_scheme_kind_from_type;
+   InSet,rec_dep_scheme_kind_from_type]
+
+let declare_one_induction_scheme ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let kind = inductive_sort_family mip in
+  let from_prop = kind = InProp in
+  let kelim = elim_sorts (mib,mip) in
+  let elims =
+    list_map_filter (fun (sort,kind) ->
+      if List.mem sort kelim then Some kind else None)
+      (if from_prop then kinds_from_prop else kinds_from_type) in
+  List.iter (fun kind -> ignore (define_individual_scheme kind true None ind))
+    elims
+
+let build_case_analysis_scheme_in_type dep ind =
+  build_case_analysis_scheme (Global.env()) Evd.empty ind dep InType
+
+let case_scheme_kind_from_type =
+  declare_individual_scheme_object "_case_nodep"
+  (build_case_analysis_scheme_in_type false)
+
+let case_scheme_kind_from_prop =
+  declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
+  (build_case_analysis_scheme_in_type false)
+
+let case_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_case" ~aux:"_case_from_type"
+  (build_case_analysis_scheme_in_type true)
+
+let case_dep_scheme_kind_from_prop =
+  declare_individual_scheme_object "_case_dep"
+  (build_case_analysis_scheme_in_type true)
+
+let declare_one_case_analysis_scheme ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let kind = inductive_sort_family mip in
+  let dep = if kind = InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+  let kelim = elim_sorts (mib,mip) in
+    (* in case the inductive has a type elimination, generates only one
+       induction scheme, the other ones share the same code with the
+       apropriate type *)
+  if List.mem InType kelim then
+    ignore (define_individual_scheme dep true None ind)
+
+let declare_induction_schemes kn =
+  let mib = Global.lookup_mind kn in
+  if mib.mind_finite then begin
+    for i = 0 to Array.length mib.mind_packets - 1 do
+      declare_one_induction_scheme (kn,i);
+    done;
+  end
+
+(* Decidable equality *)
+
+let declare_eq_decidability_gen internal names kn =
+  let mib = Global.lookup_mind kn in
+  if mib.mind_finite then
+    ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+
+let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
+  str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
+
+let declare_eq_decidability_scheme_with l kn =
+  try_declare_scheme (eq_dec_scheme_msg (kn,0))
+    declare_eq_decidability_gen false l kn
+
+let try_declare_eq_decidability kn =
+  try_declare_scheme (eq_dec_scheme_msg (kn,0))
+    declare_eq_decidability_gen true [] kn
+
+let declare_eq_decidability = declare_eq_decidability_scheme_with []
+
+let ignore_error f x = try ignore (f x) with _ -> ()
+
+let declare_rewriting_schemes ind =
+  if Hipattern.is_inductive_equality ind then begin
+    ignore (define_individual_scheme rew_r2l_scheme_kind true None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind true None ind);
+    ignore (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None ind);
+    (* These ones expect the equality to be symmetric; the first one also *)
+    (* needs eq *)
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind true None) ind;
+    ignore_error
+      (define_individual_scheme rew_l2r_dep_scheme_kind true None) ind;
+    ignore_error
+      (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None) ind
+  end
+
+let declare_congr_scheme ind =
+  if Hipattern.is_equality_type (mkInd ind) then begin
+    if
+      try Coqlib.check_required_library Coqlib.logic_module_name; true
+      with _ -> false
+    then
+      ignore (define_individual_scheme congr_scheme_kind true None ind)
+    else
+      warning "Cannot build congruence scheme because eq is not found"
+  end
+
+let declare_sym_scheme ind =
+  if Hipattern.is_inductive_equality ind then
+    (* Expect the equality to be symmetric *)
+    ignore_error (define_individual_scheme sym_scheme_kind true None) ind
+
+(* Scheme command *)
+
+let rec split_scheme l =
+ let env = Global.env() in
+ match l with
+  | [] -> [],[]
+  | (Some id,t)::q -> let l1,l2 = split_scheme q in
+    ( match t with
+      | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
+      | EqualityScheme  x -> l1,((Some id,smart_global_inductive x)::l2)
+    )
+(*
+ if no name has been provided, we build one from the types of the ind
+requested
+*)
+  | (None,t)::q ->
+       let l1,l2 = split_scheme q in
+    ( match t with
+      | InductionScheme (x,y,z) ->
+             let ind = smart_global_inductive y in
+             let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
+             let z' = family_of_sort (interp_sort z) in
+             let suffix = (
+                match sort_of_ind with
+                | InProp ->
+                    if x then (match z' with
+                       | InProp -> "_ind_nodep"
+                       | InSet -> "_rec_nodep"
+                       | InType -> "_rect_nodep")
+                    else ( match z' with
+                       | InProp -> "_ind"
+                       | InSet -> "_rec"
+                       | InType -> "_rect" )
+                | _ ->
+                    if x then (match z' with
+                       | InProp -> "_ind"
+                       | InSet -> "_rec"
+                       | InType -> "_rect" )
+                    else (match z' with
+                       | InProp -> "_ind_dep"
+                       | InSet  -> "_rec_dep"
+                       | InType -> "_rect_dep")
+                ) in
+            let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+            let newref = (dummy_loc,newid) in
+          ((newref,x,ind,z)::l1),l2
+      | EqualityScheme  x -> l1,((None,smart_global_inductive x)::l2)
+    )
+
+let do_mutual_induction_scheme lnamedepindsort =
+  let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
+  and sigma = Evd.empty
+  and env0 = Global.env() in
+  let lrecspec =
+    List.map
+      (fun (_,dep,ind,sort) -> (ind,dep,interp_elimination_sort sort))
+      lnamedepindsort
+  in
+  let listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+  let rec declare decl fi lrecref =
+    let decltype = Retyping.get_type_of env0 Evd.empty decl in
+    let decltype = refresh_universes decltype in
+    let cst = define fi false decl (Some decltype) in
+    ConstRef cst :: lrecref
+  in
+  let _ = List.fold_right2 declare listdecl lrecnames [] in
+  fixpoint_message None lrecnames
+
+let get_common_underlying_mutual_inductive = function
+  | [] -> assert false
+  | (id,(mind,i as ind))::l as all ->
+      match List.filter (fun (_,(mind',_)) -> mind <> mind') l with
+      | (_,ind')::_ ->
+	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
+      | [] ->
+	  if not (list_distinct (List.map snd (List.map snd all))) then
+	    error "A type occurs twice";
+	  mind,
+	  list_map_filter
+	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
+
+let do_scheme l =
+  let ischeme,escheme = split_scheme l in
+(* we want 1 kind of scheme at a time so we check if the user
+tried to declare different schemes at once *)
+    if (ischeme <> []) && (escheme <> [])
+    then
+      error "Do not declare equality and induction scheme at the same time."
+    else (
+      if ischeme <> [] then do_mutual_induction_scheme ischeme
+      else
+	let mind,l = get_common_underlying_mutual_inductive escheme in
+	declare_beq_scheme_with l mind;
+	declare_eq_decidability_scheme_with l mind
+    )
+
+(**********************************************************************)
+(* Combined scheme *)
+(* Matthieu Sozeau, Dec 2006 *)
+
+let list_split_rev_at index l =
+  let rec aux i acc = function
+      hd :: tl when i = index -> acc, tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "list_split_when: Invalid argument"
+  in aux 0 [] l
+
+let fold_left' f = function
+    [] -> raise (Invalid_argument "fold_left'")
+  | hd :: tl -> List.fold_left f hd tl
+
+let build_combined_scheme env schemes =
+  let defs = List.map (fun cst -> (cst, Typeops.type_of_constant env cst)) schemes in
+(*   let nschemes = List.length schemes in *)
+  let find_inductive ty =
+    let (ctx, arity) = decompose_prod ty in
+    let (_, last) = List.hd ctx in
+      match kind_of_term last with
+	| App (ind, args) ->
+	    let ind = destInd ind in
+	    let (_,spec) = Inductive.lookup_mind_specif env ind in
+	      ctx, ind, spec.mind_nrealargs
+	| _ -> ctx, destInd last, 0
+  in
+  let (c, t) = List.hd defs in
+  let ctx, ind, nargs = find_inductive t in
+  (* Number of clauses, including the predicates quantification *)
+  let prods = nb_prod t - (nargs + 1) in
+  let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+  let relargs = rel_vect 0 prods in
+  let concls = List.rev_map
+    (fun (cst, t) ->
+      mkApp(mkConst cst, relargs),
+      snd (decompose_prod_n prods t)) defs in
+  let concl_bod, concl_typ =
+    fold_left'
+      (fun (accb, acct) (cst, x) ->
+	mkApp (coqconj, [| x; acct; cst; accb |]),
+	mkApp (coqand, [| x; acct |])) concls
+  in
+  let ctx, _ =
+    list_split_rev_at prods
+      (List.rev_map (fun (x, y) -> x, None, y) ctx) in
+  let typ = it_mkProd_wo_LetIn concl_typ ctx in
+  let body = it_mkLambda_or_LetIn concl_bod ctx in
+  (body, typ)
+
+let do_combined_scheme name schemes =
+  let csts =
+    List.map (fun x ->
+		let refe = Ident x in
+		let qualid = qualid_of_reference refe in
+		try Nametab.locate_constant (snd qualid)
+                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
+      schemes
+  in
+  let body,typ = build_combined_scheme (Global.env ()) csts in
+  ignore (define (snd name) false body (Some typ));
+  fixpoint_message None [snd name]
+
+(**********************************************************************)
+
+let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
+
+let mutual_inductive_size kn = Array.length (Global.lookup_mind kn).mind_packets
+
+let declare_default_schemes kn =
+  let n = mutual_inductive_size kn in
+  if !elim_flag then declare_induction_schemes kn;
+  if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
+  if is_eq_flag() then try_declare_beq_scheme kn;
+  if !eq_dec_flag then try_declare_eq_decidability kn;
+  if !rewriting_flag then map_inductive_block declare_congr_scheme kn n;
+  if !rewriting_flag then map_inductive_block declare_sym_scheme kn n;
+  if !rewriting_flag then map_inductive_block declare_rewriting_schemes kn n
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
new file mode 100644
index 000000000..9aa32b7bd
--- /dev/null
+++ b/toplevel/indschemes.mli
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Environ
+open Libnames
+open Rawterm
+open Genarg
+open Vernacexpr
+open Ind_tables
+(*i*)
+
+(* See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
+
+(* Build and register the boolean equalities associated to an inductive type *)
+
+val declare_beq_scheme : mutual_inductive -> unit
+
+val declare_eq_decidability : mutual_inductive -> unit
+
+(* Build and register a congruence scheme for an equality-like inductive type *)
+
+val declare_congr_scheme : inductive -> unit
+
+(* Build and register rewriting schemes for an equality-like inductive type *)
+
+val declare_rewriting_schemes : inductive -> unit
+
+(* Mutual Minimality/Induction scheme *)
+
+val do_mutual_induction_scheme :
+  (identifier located * bool * inductive * rawsort) list -> unit
+
+(* Main calls to interpret the Scheme command *)
+
+val do_scheme : (identifier located option * scheme) list -> unit
+
+(* Combine a list of schemes into a conjunction of them *)
+
+val build_combined_scheme : env -> constant list -> constr * types
+
+val do_combined_scheme : identifier located -> identifier located list -> unit
+
+(* Hook called at each inductive type definition *)
+
+val declare_default_schemes : mutual_inductive -> unit
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
new file mode 100644
index 000000000..7ea001259
--- /dev/null
+++ b/toplevel/lemmas.ml
@@ -0,0 +1,299 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* Created by Hugo Herbelin from contents related to lemma proofs in
+   file command.ml, Aug 2009 *)
+
+open Util
+open Flags
+open Pp
+open Names
+open Term
+open Declarations
+open Entries
+open Environ
+open Nameops
+open Libnames
+open Decls
+open Decl_kinds
+open Declare
+open Pretyping
+open Termops
+open Evd
+open Evarutil
+open Reductionops
+open Topconstr
+open Constrintern
+open Impargs
+
+(* Support for mutually proved theorems *)
+
+let retrieve_first_recthm = function
+  | VarRef id ->
+      (pi2 (Global.lookup_named id),variable_opacity id)
+  | ConstRef cst ->
+      let {const_body=body;const_opaque=opaq} =	Global.lookup_constant cst in
+      (Option.map Declarations.force body,opaq)
+  | _ -> assert false
+
+let adjust_guardness_conditions const =
+  (* Try all combinations... not optimal *)
+  match kind_of_term const.const_entry_body with
+  | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+      let possible_indexes =
+	List.map (fun c ->
+	  interval 0 (List.length ((lam_assum c))))
+	  (Array.to_list fixdefs) in
+      let indexes =
+	search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
+      { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
+  | c -> const
+
+let look_for_mutual_statements thms =
+  if List.tl thms <> [] then
+    (* More than one statement: we look for a common inductive hyp or a *)
+    (* common coinductive conclusion *)
+    let n = List.length thms in
+    let inds = List.map (fun (id,(t,_) as x) ->
+      let (hyps,ccl) = decompose_prod_assum t in
+      let whnf_hyp_hds = map_rel_context_in_env
+        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+        (Global.env()) hyps in
+      let ind_hyps =
+        List.flatten (list_map_i (fun i (_,b,t) ->
+          match kind_of_term t with
+          | Ind (kn,_ as ind) when
+                let mind = Global.lookup_mind kn in
+                mind.mind_finite & b = None ->
+              [ind,x,i]
+          | _ ->
+              []) 1 (List.rev whnf_hyp_hds)) in
+      let ind_ccl =
+        let cclenv = push_rel_context hyps (Global.env()) in
+        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+        match kind_of_term whnf_ccl with
+        | Ind (kn,_ as ind) when
+              let mind = Global.lookup_mind kn in
+              mind.mind_ntypes = n & not mind.mind_finite ->
+            [ind,x,0]
+        | _ ->
+            [] in
+      ind_hyps,ind_ccl) thms in
+    let inds_hyps,ind_ccls = List.split inds in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
+    (* Check if all conclusions are coinductive in the same type *)
+    (* (degenerated cartesian product since there is at most one coind ccl) *)
+    let same_indccl =
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] ind_ccls in
+    let ordered_same_indccl =
+      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
+    (* Check if some hypotheses are inductive in the same type *)
+    let common_same_indhyp =
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] inds_hyps in
+    let ordered_inds,finite =
+      match ordered_same_indccl, common_same_indhyp with
+      | indccl::rest, _ ->
+	  assert (rest=[]);
+          (* One occ. of common coind ccls and no common inductive hyps *)
+	  if common_same_indhyp <> [] then
+	    if_verbose warning "Assuming mutual coinductive statements.";
+	  flush_all ();
+          indccl, true
+      | [], _::_ ->
+	  if same_indccl <> [] &&
+	     list_distinct (List.map pi1 (List.hd same_indccl)) then
+	    if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+	  (* assume the largest indices as possible *)
+	  list_last common_same_indhyp, false
+      | _, [] ->
+	  error
+            ("Cannot find common (mutual) inductive premises or coinductive" ^
+             " conclusions in the statements.")
+    in
+    let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
+    let rec_tac =
+      if finite then
+        match List.map (fun (id,(t,_)) -> (id,t)) thms with
+        | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+        | _ -> assert false
+      else
+	(* nl is dummy: it will be recomputed at Qed-time *)
+        match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+        | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+        | _ -> assert false in
+    Some rec_tac,thms
+  else
+    None, thms
+
+(* Saving a goal *)
+
+let save id const do_guard (locality,kind) hook =
+  let const = if do_guard then adjust_guardness_conditions const else const in
+  let {const_entry_body = pft;
+       const_entry_type = tpo;
+       const_entry_opaque = opacity } = const in
+  let k = logical_kind_of_goal_kind kind in
+  let l,r = match locality with
+    | Local when Lib.sections_are_opened () ->
+	let c = SectionLocalDef (pft, tpo, opacity) in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
+	(Local, VarRef id)
+    | Local | Global ->
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	Autoinstance.search_declaration (ConstRef kn);
+	(Global, ConstRef kn) in
+  Pfedit.delete_current_proof ();
+  definition_message id;
+  hook l r
+
+let save_hook = ref ignore
+let set_save_hook f = save_hook := f
+
+let save_named opacity =
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let const = { const with const_entry_opaque = opacity } in
+  save id const do_guard persistence hook
+
+let default_thm_id = id_of_string "Unnamed_thm"
+
+let compute_proof_name = function
+  | Some (loc,id) ->
+      (* We check existence here: it's a bit late at Qed time *)
+      if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+        user_err_loc (loc,"",pr_id id ++ str " already exists.");
+      id
+  | None ->
+      let rec next avoid id =
+        let id = next_global_ident_away false id avoid in
+        if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id
+        else id
+      in
+      next (Pfedit.get_all_proof_names ()) default_thm_id
+
+let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
+  match body with
+  | None ->
+      (match local with
+      | Local ->
+          let impl=false in (* copy values from Vernacentries *)
+          let k = IsAssumption Conjectural in
+          let c = SectionLocalAssum (t_i,impl) in
+	  let _ = declare_variable id (Lib.cwd(),c,k) in
+          (Local,VarRef id,imps)
+      | Global ->
+          let k = IsAssumption Conjectural in
+          let kn = declare_constant id (ParameterEntry (t_i,false), k) in
+          (Global,ConstRef kn,imps))
+  | Some body ->
+      let k = logical_kind_of_goal_kind kind in
+      let body_i = match kind_of_term body with
+        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+        | CoFix (0,decls) -> mkCoFix (i,decls)
+        | _ -> anomaly "Not a proof by induction" in
+      match local with
+      | Local ->
+	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
+	  let _ = declare_variable id (Lib.cwd(), c, k) in
+          (Local,VarRef id,imps)
+      | Global ->
+          let const =
+            { const_entry_body = body_i;
+              const_entry_type = Some t_i;
+              const_entry_opaque = opaq;
+              const_entry_boxed = false (* copy of what cook_proof does *)} in
+          let kn = declare_constant id (DefinitionEntry const, k) in
+          (Global,ConstRef kn,imps)
+
+(* 4.2| General support for goals *)
+
+let check_anonymity id save_ident =
+  if atompart_of_id id <> "Unnamed_thm" then
+    error "This command can only be used for unnamed theorem."
+(*
+    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
+*)
+
+let save_anonymous opacity save_ident =
+  let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  save save_ident const do_guard persistence hook
+
+let save_anonymous_with_strength kind opacity save_ident =
+  let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
+  let const = { const with const_entry_opaque = opacity } in
+  check_anonymity id save_ident;
+  (* we consider that non opaque behaves as local for discharge *)
+  save save_ident const do_guard (Global, Proof kind) hook
+
+(* Starting a goal *)
+
+let start_hook = ref ignore
+let set_start_hook = (:=) start_hook
+
+let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
+  let sign = Global.named_context () in
+  let sign = clear_proofs sign in
+  !start_hook c;
+  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
+
+let start_proof_com kind thms hook =
+  let evdref = ref (create_evar_defs Evd.empty) in
+  let env = Global.env () in
+  let thms = List.map (fun (sopt,(bl,t)) ->
+    let (env, ctx), imps = interp_context_evars evdref env bl in
+    let t', imps' = interp_type_evars_impls ~evdref env t in
+    let len = List.length ctx in
+      (compute_proof_name sopt,
+      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'))))
+    thms in
+  let rec_tac,thms = look_for_mutual_statements thms in
+  match thms with
+  | [] -> anomaly "No proof to start"
+  | (id,(t,(len,imps)) as thm)::other_thms ->
+      let hook strength ref =
+        let other_thms_data =
+          if other_thms = [] then [] else
+            (* there are several theorems defined mutually *)
+            let body,opaq = retrieve_first_recthm ref in
+            list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
+        let thms_data = (strength,ref,imps)::other_thms_data in
+        List.iter (fun (strength,ref,imps) ->
+	  maybe_declare_manual_implicits false ref imps;
+	  hook strength ref) thms_data in
+      let init_tac =
+       let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
+         if Flags.is_auto_intros () then
+           match rec_tac with
+           | None -> Some (intro_tac thm)
+           | Some tac -> Some (Tacticals.tclTHENS tac (List.map intro_tac thms))
+         else rec_tac
+      in start_proof id kind t ?init_tac hook ~compute_guard:(rec_tac<>None)
+
+(* Admitted *)
+
+let admit () =
+  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+  let kn =
+    declare_constant id (ParameterEntry (typ,false),IsAssumption Conjectural) in
+  Pfedit.delete_current_proof ();
+  assumption_message id;
+  hook Global (ConstRef kn)
+
+(* Miscellaneous *)
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e ->
+    (Evd.empty, Global.env())
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
new file mode 100644
index 000000000..398b336be
--- /dev/null
+++ b/toplevel/lemmas.mli
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Term
+open Decl_kinds
+open Topconstr
+open Tacexpr
+open Vernacexpr
+open Proof_type
+(*i*)
+
+(* A hook start_proof calls on the type of the definition being started *)
+val set_start_hook : (types -> unit) -> unit
+
+val start_proof : identifier -> goal_kind -> types ->
+  ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+
+val start_proof_com : goal_kind ->
+  (lident option * (local_binder list * constr_expr)) list ->
+  declaration_hook -> unit
+
+(* A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Refiner.pftreestate -> unit) -> unit
+
+(*s [save_named b] saves the current completed proof under the name it
+was started; boolean [b] tells if the theorem is declared opaque; it
+fails if the proof is not completed *)
+
+val save_named : bool -> unit
+
+(* [save_anonymous b name] behaves as [save_named] but declares the theorem
+under the name [name] and respects the strength of the declaration *)
+
+val save_anonymous : bool -> identifier -> unit
+
+(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
+   declares the theorem under the name [name] and gives it the
+   strength [strength] *)
+
+val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
+
+(* [admit ()] aborts the current goal and save it as an assmumption *)
+
+val admit : unit -> unit
+
+(* [get_current_context ()] returns the evar context and env of the
+   current open proof if any, otherwise returns the empty evar context
+   and the current global env *)
+
+val get_current_context : unit -> Evd.evar_map * Environ.env
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8bb53b378..b3fbeb655 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -9,6 +9,7 @@
 (* $Id$ *)
 
 open Pp
+open Flags
 open Util
 open Names
 open Topconstr
@@ -766,7 +767,7 @@ let find_precedence lev etyps symbols =
 	    error "The level of the leftmost non-terminal cannot be changed."
 	| ETName | ETBigint | ETReference ->
 	    if lev = None then
-	      Flags.if_verbose msgnl (str "Setting notation at level 0.")
+	      if_verbose msgnl (str "Setting notation at level 0.")
 	    else
 	    if lev <> Some 0 then
 	      error "A notation starting with an atomic expression must be at level 0.";
@@ -784,7 +785,7 @@ let find_precedence lev etyps symbols =
       (match list_last symbols with Terminal _ -> true |_ -> false)
       ->
       if lev = None then
-	(Flags.if_verbose msgnl (str "Setting notation at level 0."); 0)
+	(if_verbose msgnl (str "Setting notation at level 0."); 0)
       else Option.get lev
   | _ ->
       if lev = None then error "Cannot determine the level.";
@@ -946,12 +947,12 @@ let add_notation_in_scope local df c mods scope =
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
   (* Declare interpretation *)
   let (onlyparse,extrarecvars,recvars,vars,df') = i_data in
-  let (acvars,ac) = interp_aconstr [] (vars,recvars) c in
+  let (acvars,ac) = interp_aconstr (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
   Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
 
-let add_notation_interpretation_core local df names c scope onlyparse =
+let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
   let dfs = split_notation_string df in
   let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in
   (* Redeclare pa/pp rules *)
@@ -961,7 +962,7 @@ let add_notation_interpretation_core local df names c scope onlyparse =
   end;
   (* Declare interpretation *)
   let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
-  let (acvars,ac) = interp_aconstr names (vars,recvars) c in
+  let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
   Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
@@ -975,8 +976,12 @@ let add_syntax_extension local mv =
 
 (* Notations with only interpretation *)
 
-let add_notation_interpretation df names c sc =
-  try add_notation_interpretation_core false df names c sc false
+let add_notation_interpretation (df,c,sc) =
+  add_notation_interpretation_core false df c sc false
+
+let set_notation_for_interpretation impls (df,c,sc) =
+  Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc;
+  try silently (add_notation_interpretation_core false df ~impls c sc) false;
   with NoSyntaxRule ->
     error "Parsing rule for this notation has to be previously declared."
 
@@ -986,7 +991,7 @@ let add_notation local c (df,modifiers) sc =
   if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = modifiers=[SetOnlyParsing] in
-    try add_notation_interpretation_core local df [] c sc onlyparse
+    try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
       add_notation_in_scope local df c modifiers sc
@@ -1043,3 +1048,9 @@ let add_delimiters scope key =
 
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
+
+let add_syntactic_definition ident (vars,c) local onlyparse =
+  let ((vars,_),pat) = interp_aconstr (vars,[]) c in
+  let onlyparse = onlyparse or is_not_printable pat in
+  Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 53822b473..01c0a34da 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Util
+open Names
 open Libnames
 open Ppextend
 open Extend
@@ -41,20 +42,26 @@ val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
 (* Add only the interpretation of a notation that already has pa/pp rules *)
 
-val add_notation_interpretation : string -> Constrintern.implicits_env ->
-  constr_expr -> scope_name option -> unit
+val add_notation_interpretation :
+  (string * constr_expr * scope_name option) -> unit
+
+(* Add a notation interpretation for supporting the "where" clause *)
+
+val set_notation_for_interpretation : Constrintern.full_internalization_env ->
+  (string * constr_expr * scope_name option) -> unit
 
 (* Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
   locality_flag -> (string * syntax_modifier list) -> unit
 
-(* Print the Camlp4 state of a grammar *)
+(* Add a syntactic definition (as in "Notation f := ...") *)
 
-val print_grammar : string -> unit
+val add_syntactic_definition : identifier -> identifier list * constr_expr ->
+  bool -> bool -> unit
 
-(* Evaluate whether a notation is not printable *)
+(* Print the Camlp4 state of a grammar *)
 
-val is_not_printable : aconstr -> bool
+val print_grammar : string -> unit
 
 val check_infix_modifiers : syntax_modifier list -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e11a3b373..1a3e5102e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -31,33 +31,27 @@ open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let interp_evars evdref env ?(impls=([],[])) k typ =
+let interp_evars evdref env impls k typ =
+  let impls = set_internalization_env_params impls [] in
   let typ' = intern_gen true ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
 
-let mk_interning_data env na impls typ =
-  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
-  in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
-
 let interp_fields_evars evars env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
-      let impl, t' = interp_evars evars env ~impls Pretyping.IsType t in
-      let b' = Option.map (fun x -> snd (interp_evars evars env ~impls (Pretyping.OfType (Some t')) x)) b in
+      let impl, t' = interp_evars evars env impls Pretyping.IsType t in
+      let b' = Option.map (fun x -> snd (interp_evars evars env impls (Pretyping.OfType (Some t')) x)) b in
       let impls =
 	match i with
 	| Anonymous -> impls
-	| Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls)
+	| Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
       in
       let d = (i,b',t') in
-	(* Temporary declaration of notations and scopes *)
-	Option.iter (fun ((_,_,sc) as x) ->
-          declare_interning_data impls x;
-          open_temp_scopes sc
-        ) no;
-	(push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], ([], [])) nots l
+      let impls' = set_internalization_env_params impls [] in
+      Option.iter (Metasyntax.set_notation_for_interpretation impls') no;
+      (push_rel d env, impl :: uimpls, d::params, impls))
+    (env, [], [], []) nots l
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -267,7 +261,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_record = true;
       mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
-  let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations true mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
@@ -343,7 +337,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
-	  (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *)
 	  IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
 			     (List.rev fields) (Recordops.lookup_projections ind))
   in
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 1d20106a5..daca81757 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -7,6 +7,8 @@ Auto_ind_decl
 Libtypes
 Search
 Autoinstance
+Lemmas
+Indschemes
 Command
 Classes
 Record
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d2a9153fe..3d7751d97 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -36,6 +36,7 @@ open Topconstr
 open Pretyping
 open Redexpr
 open Syntax_def
+open Lemmas
 
 (* Pcoq hooks *)
 
@@ -306,7 +307,7 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+let vernac_definition (local,boxed,k) (loc,id as lid) def hook =
   Dumpglob.dump_definition lid false "def";
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
@@ -321,9 +322,10 @@ let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
  	let red_option = match red_option with
           | None -> None
           | Some r ->
- 	      let (evc,env)= Command.get_current_context () in
+	      let (evc,env)= get_current_context () in
  		Some (interp_redexp env evc r) in
- 	  declare_definition id k bl red_option c typ_opt hook)
+	let ce,imps = interp_definition boxed bl red_option c typ_opt in
+	declare_definition id (local,k) ce imps hook)
 
 let vernac_start_proof kind l lettop hook =
   if Dumpglob.dump () then
@@ -363,13 +365,17 @@ let vernac_exact_proof c =
 	(strbrk "Command 'Proof ...' can only be used at the beginning of the proof.")
 
 let vernac_assumption kind l nl=
+  if Pfedit.refining () then
+    errorlabstrm ""
+      (str "Cannot declare an assumption while in proof editing mode.");
   let global = fst kind = Global in
     List.iter (fun (is_coe,(idl,c)) ->
       if Dumpglob.dump () then
 	List.iter (fun lid ->
 	  if global then Dumpglob.dump_definition lid false "ax"
 	  else Dumpglob.dump_definition lid true "var") idl;
-      declare_assumption idl is_coe kind [] c false nl) l
+      let t,imps = interp_assumption [] c in
+      declare_assumptions idl is_coe kind t imps false nl) l
 
 let vernac_record k finite infer struc binders sort nameopt cfs =
   let const = match nameopt with
@@ -414,21 +420,21 @@ let vernac_inductive finite infer indl =
       | _ -> Util.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-      Command.build_mutual indl (recursivity_flag_of_kind finite)
+    do_mutual_inductive indl (recursivity_flag_of_kind finite)
 
 let vernac_fixpoint l b =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  build_recursive l b
+  do_fixpoint l b
 
 let vernac_cofixpoint l b =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  build_corecursive l b
+  do_cofixpoint l b
 
-let vernac_scheme = build_scheme
+let vernac_scheme = Indschemes.do_scheme
 
-let vernac_combined_scheme = build_combined_scheme
+let vernac_combined_scheme = Indschemes.do_combined_scheme
 
 (**********************)
 (* Modules            *)
@@ -761,7 +767,7 @@ let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h)
 
 let vernac_syntactic_definition lid =
   Dumpglob.dump_definition lid false "syndef";
-  Command.syntax_definition (snd lid)
+  Metasyntax.add_syntactic_definition (snd lid)
 
 let vernac_declare_implicits local r = function
   | Some imps ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9bcdd402d..c590202e5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -155,11 +155,11 @@ type local_decl_expr =
   | DefExpr of lname * constr_expr * constr_expr option
 
 type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
-type decl_notation = (string * constr_expr * scope_name option) option
+type decl_notation = string * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
-type 'a with_notation = 'a * decl_notation
+type 'a with_notation = 'a * decl_notation option
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
@@ -168,6 +168,9 @@ type inductive_expr =
   lident with_coercion * local_binder list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
 
+type one_inductive_expr =
+  lident * local_binder list * constr_expr option * constructor_expr list
+
 type module_binder = bool option * lident list * module_type_ast
 
 type grammar_tactic_prod_item_expr =
@@ -220,9 +223,9 @@ type vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
-  | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation) list
-  | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
-  | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
+  | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation option) list
+  | VernacFixpoint of (fixpoint_expr * decl_notation option) list * bool
+  | VernacCoFixpoint of (cofixpoint_expr * decl_notation option) list * bool
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
 
@@ -387,7 +390,7 @@ let enforce_locality_full local =
     | None ->
 	if local then begin
 	  Flags.if_verbose
-	    Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
+	   Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
 	  Some true
 	end else
 	None
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 0d4168ec6..98a79a9ce 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -185,7 +185,7 @@ let whelp_constr req c =
   send_whelp req (make_string uri_of_constr c)
 
 let whelp_constr_expr req c =
-  let (sigma,env)= get_current_context () in
+  let (sigma,env)= Lemmas.get_current_context () in
   let _,c = interp_open_constr sigma env c in
   whelp_constr req c