modules Indrec, Tacentries, Hiddentac

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

28 files changed, 591 insertions, 287 deletions

diff --git a/.depend b/.depend
index f215a33d94..838153f837 100644
--- a/.depend
+++ b/.depend
@@ -20,7 +20,8 @@ kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi 
 kernel/sosub.cmi: kernel/term.cmi 
-kernel/term.cmi: kernel/generic.cmi kernel/names.cmi kernel/univ.cmi 
+kernel/term.cmi: kernel/generic.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/univ.cmi 
 kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
 kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
@@ -81,11 +82,14 @@ proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
 proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 tactics/btermdn.cmi: kernel/generic.cmi kernel/term.cmi 
 tactics/dn.cmi: lib/tlm.cmi 
+tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_trees.cmi \
+    tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi kernel/term.cmi \
     tactics/termdn.cmi 
 tactics/pattern.cmi: kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi tactics/stock.cmi kernel/term.cmi lib/util.cmi 
 tactics/stock.cmi: kernel/names.cmi 
+tactics/tacentries.cmi: proofs/proof_trees.cmi proofs/tacmach.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi tactics/pattern.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
@@ -254,12 +258,14 @@ library/impargs.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     library/global.cmx kernel/inductive.cmx kernel/names.cmx \
     kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
     kernel/typing.cmx library/impargs.cmi 
-library/indrec.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
-    kernel/term.cmi kernel/typing.cmi lib/util.cmi library/indrec.cmi 
-library/indrec.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
-    kernel/term.cmx kernel/typing.cmx lib/util.cmx library/indrec.cmi 
+library/indrec.cmo: kernel/environ.cmi kernel/generic.cmi \
+    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
+    kernel/typeops.cmi lib/util.cmi library/indrec.cmi 
+library/indrec.cmx: kernel/environ.cmx kernel/generic.cmx \
+    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
+    kernel/typeops.cmx lib/util.cmx library/indrec.cmi 
 library/lib.cmo: library/libobject.cmi kernel/names.cmi library/summary.cmi \
     lib/util.cmi library/lib.cmi 
 library/lib.cmx: library/libobject.cmx kernel/names.cmx library/summary.cmx \
@@ -400,24 +406,32 @@ tactics/btermdn.cmx: tactics/dn.cmx kernel/term.cmx tactics/termdn.cmx \
     tactics/btermdn.cmi 
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
+tactics/hiddentac.cmo: proofs/proof_trees.cmi tactics/tacentries.cmi \
+    proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi 
+tactics/hiddentac.cmx: proofs/proof_trees.cmx tactics/tacentries.cmx \
+    proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi 
 tactics/nbtermdn.cmo: tactics/btermdn.cmi kernel/generic.cmi lib/gmap.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi 
 tactics/nbtermdn.cmx: tactics/btermdn.cmx kernel/generic.cmx lib/gmap.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi 
-tactics/pattern.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/evd.cmi \
-    kernel/generic.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sosub.cmi \
-    tactics/stock.cmi kernel/term.cmi tactics/pattern.cmi 
-tactics/pattern.cmx: parsing/astterm.cmi proofs/clenv.cmx kernel/evd.cmx \
-    kernel/generic.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \
-    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sosub.cmx \
-    tactics/stock.cmx kernel/term.cmx tactics/pattern.cmi 
+tactics/pattern.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi kernel/names.cmi parsing/pcoq.cmi \
+    lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sosub.cmi \
+    tactics/stock.cmi kernel/term.cmi lib/util.cmi tactics/pattern.cmi 
+tactics/pattern.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx kernel/names.cmx parsing/pcoq.cmi \
+    lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sosub.cmx \
+    tactics/stock.cmx kernel/term.cmx lib/util.cmx tactics/pattern.cmi 
 tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
     kernel/names.cmi lib/pp.cmi lib/util.cmi tactics/stock.cmi 
 tactics/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
     kernel/names.cmx lib/pp.cmx lib/util.cmx tactics/stock.cmi 
+tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi 
+tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi 
 tactics/tacticals.cmo: proofs/clenv.cmi library/declare.cmi \
     kernel/environ.cmi kernel/generic.cmi library/global.cmi \
     library/indrec.cmi kernel/inductive.cmi kernel/names.cmi \
@@ -429,7 +443,7 @@ tactics/tacticals.cmx: proofs/clenv.cmx library/declare.cmx \
     library/indrec.cmx kernel/inductive.cmx kernel/names.cmx \
     tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
-    lib/util.cmx tactics/wcclausenv.cmi tactics/tacticals.cmi 
+    lib/util.cmx tactics/wcclausenv.cmx tactics/tacticals.cmi 
 tactics/tactics.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/indrec.cmi \
     kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \
@@ -448,6 +462,14 @@ tactics/termdn.cmo: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi \
     lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/generic.cmx kernel/term.cmx \
     lib/util.cmx tactics/termdn.cmi 
+tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi proofs/logic.cmi kernel/names.cmi \
+    lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi tactics/wcclausenv.cmi 
+tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx proofs/logic.cmx kernel/names.cmx \
+    lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
diff --git a/Makefile b/Makefile
index c2197c9944..8791b0c453 100644
--- a/Makefile
+++ b/Makefile
@@ -56,7 +56,8 @@ PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \
 
 TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \
-	tactics/wcclausenv.cmo tactics/tacticals.cmo \
+	tactics/wcclausenv.cmo tactics/tacticals.cmo tactics/tactics.cmo \
+        tactics/tacentries.cmo tactics/hiddentac.cmo
 
 PRETYPING=pretyping/astterm.cmo
 
diff --git a/dev/changements.txt b/dev/changements.txt
index 427ac393e6..0e0ae4f1c5 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -46,6 +46,7 @@ Changements dans les fonctions :
 	  rev_append	 ->  List.rev_append
 
 	Termenv
+	  mind_specif_of_mind  ->  Global.lookup_mind_specif
 	  mis_arity      ->  instantiate_arity
 	  mis_lc	 ->  instantiate_lc	
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index db5458211d..96fe8d5846 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -110,7 +110,7 @@ let listrec_mconstr env ntypes nparams i indlc =
     let (lpar,auxlargs) = array_chop auxnpar largs in 
     if not (array_for_all (noccur_bet n ntypes) auxlargs) then
       raise (InductiveError (NonPos n));
-    let auxlc = mis_lc env mispeci 
+    let auxlc = mis_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
     if auxntyp <> 1 then raise (InductiveError (NonPos n));
     let lrecargs = array_map_to_list (check_param_pos n) lpar in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d9a11fe478..ceb8fa0deb 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -56,6 +56,7 @@ val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 val mis_recarg : mind_specif -> (recarg list) array
 val mis_typename : mind_specif -> identifier
+val is_recursive : int list -> recarg list array -> bool
 val mis_is_recursive : mind_specif -> bool
 
 val mind_nth_type_packet : 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 0cdc50c562..07c5525263 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -60,10 +60,28 @@ let const_abst_opt_value env c =
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
 
-let mis_lc env mis =
+let mis_lc mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
     (Array.to_list mis.mis_args)
 
+let mis_lc_without_abstractions mis = 
+  let rec strip_DLAM = function
+    | (DLAM (n,c1)) -> strip_DLAM c1 
+    | (DLAMV (n,v)) -> v
+    | _ -> assert false
+  in 
+  strip_DLAM (mis_lc mis)
+
+let mis_type_mconstructs mispec =
+  let specif = mis_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) 
+  and make_Ck k = DOPN(MutConstruct((mispec.mis_sp,mispec.mis_tyi),k+1),
+		       mispec.mis_args) in
+  (Array.init nconstr make_Ck, 
+   sAPPVList specif (list_tabulate make_Ik ntypes))
+
 (* Existentials. *)
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
@@ -83,3 +101,14 @@ let existential_value sigma c =
 	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
     | Evar_empty ->
 	anomaly "a defined existential with no body"
+
+let mis_arity' mis =
+  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
+  and largs = Array.to_list mis.mis_args in 
+  { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs;
+    typ = mis.mis_mip.mind_arity.typ }
+
+let mis_arity mispec =
+  let { body = b; typ = t } = mis_arity' mispec in
+  DOP2 (Cast, b, DOP0 (Sort t))
+
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 27bd8191ec..ba5a072a1e 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -24,5 +24,10 @@ val existential_type : 'a evar_map -> constr -> constr
 
 val const_abst_opt_value : unsafe_env -> constr -> constr option
 
-val mis_lc : unsafe_env -> mind_specif -> constr
+val mis_arity : mind_specif -> constr
+
+val mis_lc : mind_specif -> constr
+val mis_lc_without_abstractions : mind_specif -> constr array
+
+val mis_type_mconstructs : mind_specif -> constr array * constr array
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1a1ea5bbb4..0d4557efc6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -310,9 +310,8 @@ let fold_commands cl env sigma c =
 
 let abstract_scheme env (locc,a,ta) t =
   let na = named_hd env ta Anonymous in
-  if occur_meta ta then
-    error "cannot find a type for the generalisation"
-  else if occur_meta a then 
+  if occur_meta ta then error "cannot find a type for the generalisation";
+  if occur_meta a then 
     DOP2(Lambda,ta,DLAM(na,t))
   else 
     DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t))
diff --git a/kernel/term.ml b/kernel/term.ml
index 4694a75a25..543c41baa8 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -52,6 +52,11 @@ type sorts =
 let mk_Set  = Prop Pos
 let mk_Prop = Prop Null
 
+let print_sort = function
+  | Prop Pos -> [< 'sTR "Set" >]
+  | Prop Null -> [< 'sTR "Prop" >]
+  | Type _ -> [< 'sTR "Type" >]
+
 type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
diff --git a/kernel/term.mli b/kernel/term.mli
index 5f8cfefc01..823917ea5f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Pp
 open Names
 open Generic
 (*i*)
@@ -39,6 +40,8 @@ type sorts =
 val mk_Set  : sorts
 val mk_Prop : sorts
 
+val print_sort : sorts -> std_ppcmds
+
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating the generic terms (type [term], 
   see \refsec{generic_terms}) on the above operators, themselves instanciated
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c072a368b4..db992769dd 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -26,6 +26,8 @@ type type_error =
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
+  | NotInductive of constr
+  | MLCase of string * constr * constr * constr * constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -71,4 +73,8 @@ let error_ill_formed_rec_body k env str lna i vdefs =
 let error_ill_typed_rec_body k env i lna vdefj vargs =
   raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
+let error_not_inductive k env c =
+  raise (TypeError (k, context env, NotInductive c))
 
+let error_ml_case k env mes c ct br brt =
+  raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt)))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 961a1b2511..fae63666c1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -28,6 +28,8 @@ type type_error =
   | IllFormedRecBody of std_ppcmds * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * typed_type array
+  | NotInductive of constr
+  | MLCase of string * constr * constr * constr * constr
 
 exception TypeError of path_kind * context * type_error
 
@@ -72,3 +74,8 @@ val error_ill_typed_rec_body  :
   path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> 'b
 
+val error_not_inductive : path_kind -> unsafe_env -> constr -> 'a
+
+val error_ml_case : path_kind -> unsafe_env -> 
+  string -> constr -> constr -> constr -> constr -> 'a
+
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 010dde8e27..65406f2798 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -150,6 +150,31 @@ let type_mconstructs env sigma mind =
   let mis = lookup_mind_specif redmind env in 
   mis_type_mconstructs mis
 
+let mis_type_mconstruct i mispec =
+  let specif = instantiate_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in 
+  if i > nconstr then error "Not enough constructors in the type";
+  sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+
+let type_mconstruct env sigma i mind =
+  let redmind = check_mrectype_spec env sigma mind in
+  let (sp,tyi,args) = destMutInd redmind in
+  let mispec = lookup_mind_specif redmind env in 
+  mis_type_mconstruct i mispec
+
+let type_inst_construct env sigma i mind = 
+  try 
+    let (mI,largs) = find_mrectype env sigma mind in 
+    let mispec = lookup_mind_specif mI env in 
+    let nparams = mis_nparams mispec in 
+    let tc = mis_type_mconstruct i mispec in
+    let (globargs,_) = list_chop nparams largs in
+    hnf_prod_applist env sigma "Typing.type_construct" tc globargs
+  with Induc -> 
+    error_not_inductive CCI env mind
+
 (* Case. *)
 
 let rec sort_of_arity env sigma c =
@@ -221,8 +246,10 @@ let is_correct_arity env sigma kelim (c,p) =
 	   (fun s -> make_arity_dep env sigma (DOP0(Sort s)) t ind) kelim)
 	@(List.map 
 	    (fun s -> make_arity_nodep env sigma (DOP0(Sort s)) t) kelim)
-      in error_elim_arity CCI env ind listarity c p pt kinds
-  in srec 
+      in 
+      error_elim_arity CCI env ind listarity c p pt kinds
+  in 
+  srec 
 
 let cast_instantiate_arity mis =
   let tty = instantiate_arity mis in
@@ -291,15 +318,12 @@ let type_case_branches env sigma ct pt p c =
 let check_branches_message env sigma (c,ct) (explft,lft) = 
   let n = Array.length explft 
   and expn = Array.length lft in
-  let rec check_conv i = 
-    if not (i = n) then
-      if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
-	error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
-	  (nf_betaiota env sigma explft.(i))
-      else 
-	check_conv (i+1) 
-  in
-  if n<>expn then error_number_branches CCI env c ct expn else check_conv 0
+  if n<>expn then error_number_branches CCI env c ct expn;
+  for i = 0 to n-1 do
+    if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
+      error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
+	(nf_betaiota env sigma explft.(i))
+  done
 
 let type_of_case env sigma pj cj lfj =
   let lft = Array.map (fun j -> j.uj_type) lfj in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cb7f97ec57..45db129741 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 (*i*)
@@ -66,3 +65,22 @@ val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
 
 val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
+
+val type_one_branch_dep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr -> constr 
+
+val type_one_branch_nodep : unsafe_env -> 'a evar_map -> 
+  int * constr list * constr -> constr -> constr 
+
+val make_arity_dep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
+
+val make_arity_nodep : 
+  unsafe_env -> 'a evar_map -> constr -> constr -> constr 
+
+val find_case_dep_nparams :
+  unsafe_env -> 'a evar_map -> constr * constr ->
+    constr * constr list ->
+      constr -> bool * (int * constr list * constr list) 
+
+val type_inst_construct : unsafe_env -> 'a evar_map -> int -> constr -> constr 
diff --git a/lib/util.ml b/lib/util.ml
index 46474ad936..7f726fe0ed 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -73,7 +73,7 @@ let list_chop n l =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
-    | (_, []) -> failwith "chop_list"
+    | (_, []) -> failwith "list_chop"
   in 
   chop_aux [] (n,l)
 
@@ -109,8 +109,8 @@ let list_fold_left_i f =
   let rec it_list_f i a = function
     | [] -> a 
     | b::l -> it_list_f (i+1) (f i a b) l
- in 
- it_list_f 
+  in 
+  it_list_f 
 
 let list_for_all_i p = 
   let rec for_all_p i = function
@@ -182,6 +182,14 @@ let list_lastn n l =
   in
   if len < n then failwith "lastn" else aux len l
 
+let list_prefix_of prefl l = 
+  let rec prefrec = function
+    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
+    | ([], _) -> true
+    | (_, _) -> false
+  in 
+  prefrec (prefl,l)
+    
 (* Arrays *)
 
 let array_exists f v = 
@@ -228,20 +236,16 @@ let array_fold_left2 f a v1 v2 =
   let rec fold a n = 
     if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n)
   in
-  if Array.length v2 <> lv1 then
-    invalid_arg "array_fold_left2"
-  else
-    fold a 0
+  if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
+  fold a 0
 
 let array_fold_left2_i f a v1 v2 =
   let lv1 = Array.length v1 in
   let rec fold a n = 
     if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n)
   in
-  if Array.length v2 <> lv1 then
-    invalid_arg "array_fold_left2"
-  else
-    fold a 0
+  if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
+  fold a 0
 
 let array_fold_left_from n f a v = 
   let rec fold a n =
@@ -256,31 +260,24 @@ let array_fold_right_from n f v a =
   fold n
 
 let array_app_tl v l = 
-  if Array.length v = 0 then 
-    invalid_arg "array_app_tl"
-  else 
-    array_fold_right_from 1 (fun e l -> e::l) v l
+  if Array.length v = 0 then invalid_arg "array_app_tl";
+  array_fold_right_from 1 (fun e l -> e::l) v l
 
 let array_list_of_tl v =
-  if Array.length v = 0 then 
-    invalid_arg "array_list_of_tl"
-  else 
-    array_fold_right_from 1 (fun e l -> e::l) v []
+  if Array.length v = 0 then invalid_arg "array_list_of_tl";
+  array_fold_right_from 1 (fun e l -> e::l) v []
 
 let array_map_to_list f v =
   List.map f (Array.to_list v)
 
 let array_chop n v =
   let vlen = Array.length v in
-  if n > vlen then 
-    failwith "chop_vect"
-  else 
-    (Array.sub v 0 n, Array.sub v n (vlen-n))
+  if n > vlen then failwith "array_chop";
+  (Array.sub v 0 n, Array.sub v n (vlen-n))
 
 let array_map2 f v1 v2 =
-  if Array.length v1 <> Array.length v2 then
-    invalid_arg "map2_vect"
-  else if Array.length v1 == 0 then 
+  if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
+  if Array.length v1 == 0 then 
     [| |] 
   else begin
     let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
@@ -290,6 +287,19 @@ let array_map2 f v1 v2 =
     res
   end
 
+let array_map3 f v1 v2 v3 =
+  if Array.length v1 <> Array.length v2 ||
+     Array.length v1 <> Array.length v3 then invalid_arg "array_map3";
+  if Array.length v1 == 0 then 
+    [| |] 
+  else begin
+    let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in
+    for i = 1 to pred (Array.length v1) do
+      res.(i) <- f v1.(i) v2.(i) v3.(i)
+    done;
+    res
+  end
+
 (* Functions *)
 
 let compose f g x = f (g x)
diff --git a/lib/util.mli b/lib/util.mli
index 1952dc46cd..77c87c5288 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -53,6 +53,7 @@ val list_subset : 'a list -> 'a list -> bool
 val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_firstn : int -> 'a list -> 'a list
 val list_lastn : int -> 'a list -> 'a list
+val list_prefix_of : 'a list -> 'a list -> bool
 
 (*s Arrays. *)
 
@@ -74,6 +75,8 @@ val array_list_of_tl : 'a array -> 'a list
 val array_map_to_list : ('a -> 'b) -> 'a array ->'b list
 val array_chop : int -> 'a array -> 'a array * 'a array
 val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
+val array_map3 : 
+  ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
 
 (*s Functions. *)
 
diff --git a/library/declare.ml b/library/declare.ml
index ff006625a1..00f1fbf8d8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -175,7 +175,7 @@ let global_reference kind id =
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
-    prefix_of (dirpath osp) (Lib.cwd())
+    list_prefix_of (dirpath osp) (Lib.cwd())
   with Not_found -> 
     false
 
diff --git a/library/global.ml b/library/global.ml
index 63efdbe4d9..e6c4008067 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Util
 open Generic
 open Term
 open Instantiate
@@ -52,29 +53,9 @@ let mind_is_recursive = Util.compose mis_is_recursive lookup_mind_specif
 let mind_nconstr = Util.compose mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose mis_nparams lookup_mind_specif
 
-let mis_arity' mis =
-  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in 
-  { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs;
-    typ = mis.mis_mip.mind_arity.typ }
-
-let mis_arity mispec =
-  let { body = b; typ = t } = mis_arity' mispec in
-  DOP2 (Cast, b, DOP0 (Sort t))
-
 let mind_arity = Util.compose mis_arity lookup_mind_specif
 
-let mis_lc mis = 
-  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps)
-    mis.mis_mip.mind_lc (Array.to_list mis.mis_args)
-
-let mis_lc_without_abstractions mis = 
-  let rec strip_DLAM = function
-    | (DLAM (n,c1)) -> strip_DLAM c1 
-    | (DLAMV (n,v)) -> v
-    | _ -> assert false
-  in 
-  strip_DLAM (mis_lc mis)
-
 let mind_lc_without_abstractions = 
   Util.compose mis_lc_without_abstractions lookup_mind_specif
+
+
diff --git a/library/global.mli b/library/global.mli
index 5a788f1f93..4e186d35b5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -48,4 +48,3 @@ val mind_arity : constr -> constr
 
 val mind_lc_without_abstractions : constr -> constr array
 
-
diff --git a/library/indrec.ml b/library/indrec.ml
index 788e405f95..3aaa2214d9 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -7,11 +7,11 @@ open Names
 open Generic
 open Term
 open Inductive
+open Instantiate
 open Environ
 open Reduction
-open Typing
-
-let whd_betadeltaiota_empty env = whd_betadeltaiota env Evd.empty
+open Typeops
+open Type_errors
 
 let make_lambda_string s t c = DOP2(Lambda,t,DLAM(Name(id_of_string s),c))
 
@@ -21,60 +21,59 @@ let lift_context n l =
   let k = List.length l in 
   list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
 
+let prod_create env (a,b) = 
+  mkProd (named_hd env a Anonymous) a b
+let lambda_name env (n,a,b) = 
+  mkLambda (named_hd env a n) a b
+let lambda_create env (a,b) = 
+  mkLambda (named_hd env a Anonymous) a b
+let it_prod_name env = 
+  List.fold_left (fun c (n,t) -> prod_name env (n,t,c)) 
+let it_lambda_name env = 
+  List.fold_left (fun c (n,t) -> lambda_name env (n,t,c))
+
 (*******************************************)
 (* Building curryfied elimination          *)
 (*******************************************)
 
-(*********************************************)
-(* lc is the list of the constructors of ind *)
-(*********************************************)
+(* (lc is the list of the constructors of ind) *)
 
-let mis_make_case_com depopt sigma mispec kinds =
+let mis_make_case_com depopt env sigma mispec kinds =
   let sp = mispec.mis_sp in
   let tyi = mispec.mis_tyi in 
   let cl = mispec.mis_args in 
   let nparams = mis_nparams mispec in
   let mip = mispec.mis_mip in
   let mind = DOPN(MutInd(sp,tyi),cl) in
-  let kd = mis_kd mispec in
-  let kn = mis_kn mispec in
+  let kelim = mis_kelim mispec in
   let t = mis_arity mispec in
   let (lc,lct) = mis_type_mconstructs mispec in
-  let lnames,sort = splay_prod sigma t in
+  let lnames,sort = splay_prod env sigma t in
   let nconstr = Array.length lc in
   let dep = match depopt with 
     | None -> (sort<>DOP0(Sort(Prop Null)))
     | Some d -> d
   in
-  let _ =
-    if dep then begin
-      if not (List.exists (sort_cmp CONV_X kinds) kd) then 
-       	let pm = pTERM mind in
-       	let ps = pTERM (DOP0(Sort kinds)) in
-       	errorlabstrm "Case analysis"
-          [< 'sTR "Dependent case analysis on sort: "; ps; 'fNL;
-             'sTR "is not allowed for inductive definition: "; pm >]
-    end else if not (List.exists (sort_cmp CONV_X kinds) kn) then 
-      let pm = pTERM mind in
-      let ps = pTERM (DOP0(Sort kinds)) in
-      errorlabstrm "Case analysis"
-       	[< 'sTR "Non Dependent case analysis on sort: "; ps; 'fNL;
-           'sTR "is not allowed for inductive definition: "; pm >]
-  in
-  let lnamesar,lnamespar = chop_list (List.length lnames - nparams) lnames in
+  if not (List.exists (base_sort_cmp CONV kinds) kelim) then begin
+    errorlabstrm "Case analysis"
+      [< 'sTR (if dep then "Dependent" else "Non Dependent");
+	 'sTR " case analysis on sort: "; print_sort kinds; 'fNL;
+         'sTR "is not allowed for inductive definition: "; print_sp sp >]
+  end;
+  let lnamesar,lnamespar = list_chop (List.length lnames - nparams) lnames in
   let lgar = List.length lnamesar in
-  let ar = hnf_prod_appvect sigma "make_case_dep" t (rel_vect 0 nparams) in
+  let ar = hnf_prod_appvect env sigma "make_case_dep" t (rel_vect 0 nparams) in
   let typP = 
     if dep then 
-      make_arity_dep (DOP0(Sort kinds)) ar 
+      make_arity_dep env sigma (DOP0(Sort kinds)) ar 
        	(appvect (mind,rel_vect 0 nparams))
     else 
-      make_arity_nodep (DOP0(Sort kinds)) ar 
+      make_arity_nodep env sigma (DOP0(Sort kinds)) ar 
   in 
   let rec add_branch k = 
     if k = nconstr then 
-      it_lambda_name 
-       	(lambda_create 
+      it_lambda_name env
+       	(lambda_create env
            (appvect (mind,
                      (Array.append (rel_vect (nconstr+lgar+1) nparams)
                        	(rel_vect 0 lgar))),
@@ -89,20 +88,19 @@ let mis_make_case_com depopt sigma mispec kinds =
     else 
       make_lambda_string "f" 
        	(if dep then 
-	   type_one_branch_dep 
-             (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k)
+	   type_one_branch_dep env sigma
+             (nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k)
          else 
-	  type_one_branch_nodep 
-            (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k))
+	  type_one_branch_nodep env sigma
+            (nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k))
        	(add_branch (k+1))
   in 
-  it_lambda_name (make_lambda_string "P" typP (add_branch 0)) lnamespar
+  it_lambda_name env (make_lambda_string "P" typP (add_branch 0)) lnamespar
     
-let make_case_com depopt sigma mind kinds =
-  let ity = mrectype_spec sigma mind in
-  let (sp,tyi,cl) = destMutInd ity in
-  let mispec = mind_specif_of_mind ity in 
-  mis_make_case_com depopt sigma mispec kinds
+let make_case_com depopt env sigma mind kinds =
+  let ity = mrectype_spec env sigma mind in
+  let mispec = lookup_mind_specif ity env in 
+  mis_make_case_com depopt env sigma mispec kinds
 
 let make_case_dep sigma   = make_case_com (Some true) sigma
 let make_case_nodep sigma = make_case_com (Some false) sigma 
@@ -126,18 +124,18 @@ let make_case_gen sigma   = make_case_com None sigma
 ************************************************************************)
 
 let simple_prod (n,t,c) = DOP2(Prod,t,DLAM(n,c))
-let make_prod_dep dep = if dep then prod_name else simple_prod
+let make_prod_dep dep env = if dep then prod_name env else simple_prod
 
-let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs = 
+let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs = 
   let make_prod = make_prod_dep dep in
   let nparams = Array.length vargs in
-  let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in
+  let st = hnf_prod_appvect env sigma "type_rec_branch" t vargs in
   let process_pos depK pk = 
     let rec prec i p = 
-      match whd_betadeltaiota_stack sigma p [] with 
-	| (DOP2(Prod,t,DLAM(n,c))),[] -> make_prod (n,t,prec (i+1) c)
+      match whd_betadeltaiota_stack env sigma p [] with 
+	| (DOP2(Prod,t,DLAM(n,c))),[] -> make_prod env (n,t,prec (i+1) c)
      	| (DOPN(MutInd _,_),largs) -> 
-	    let (_,realargs) = chop_list nparams largs in 
+	    let (_,realargs) = list_chop nparams largs in 
 	    let base = applist (lift i pk,realargs) in       
             if depK then 
 	      mkAppList base [appvect (Rel (i+1),rel_vect 0 i)]
@@ -148,7 +146,7 @@ let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs =
     prec 0 
   in
   let rec process_constr i c recargs co = 
-    match whd_betadeltaiota_stack sigma c [] with 
+    match whd_betadeltaiota_stack env sigma c [] with 
       | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> 
           let (optionpos,rest) = 
 	    match recargs with 
@@ -161,34 +159,34 @@ let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs =
 	  in 
           (match optionpos with 
 	     | None -> 
-		 make_prod (n,t,process_constr (i+1) c_0 rest 
-                              (mkAppList (lift 1 co) [Rel 1]))
+		 make_prod env (n,t,process_constr (i+1) c_0 rest 
+				  (mkAppList (lift 1 co) [Rel 1]))
              | Some(dep',p) -> 
 		 let nP = lift (i+1+decP) p in
 		 let t_0 = process_pos dep' nP (lift 1 t) in 
-		 make_prod_dep (dep or dep')
+		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
 				       (mkAppList (lift 2 co) [Rel 2]))))
       | (DOPN(MutInd(_,tyi),_),largs) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
 	    | _ -> assert false in
-      	  let (_,realargs) = chop_list nparams largs in
+      	  let (_,realargs) = list_chop nparams largs in
       	  let base = applist (nP,realargs) in
           if dep then mkAppList base [co] else base
       | _ -> assert false
   in 
   process_constr 0 st recargs (appvect(co,vargs))
 
-let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs = 
+let rec_branch_arg env sigma (vargs,fvect,decF) f t recargs = 
   let nparams = Array.length vargs in
-  let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in
+  let st = hnf_prod_appvect env sigma "type_rec_branch" t vargs in
   let process_pos fk  = 
     let rec prec i p = 
-      (match whd_betadeltaiota_stack sigma p [] with 
-	 | (DOP2(Prod,t,DLAM(n,c))),[] -> lambda_name (n,t,prec (i+1) c) 
+      (match whd_betadeltaiota_stack env sigma p [] with 
+	 | (DOP2(Prod,t,DLAM(n,c))),[] -> lambda_name env (n,t,prec (i+1) c) 
      	 | (DOPN(MutInd _,_),largs) -> 
-             let (_,realargs) = chop_list nparams largs
+             let (_,realargs) = list_chop nparams largs
              and arg = appvect (Rel (i+1),rel_vect 0 i) in 
              applist(lift i fk,realargs@[arg])
      	 | _ -> assert false) 
@@ -196,7 +194,7 @@ let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs =
     prec 0 
   in
   let rec process_constr i c f recargs = 
-    match whd_betadeltaiota_stack sigma c [] with 
+    match whd_betadeltaiota_stack env sigma c [] with 
       | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> 
           let (optionpos,rest) = 
 	    match recargs with 
@@ -208,29 +206,31 @@ let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs =
 	  in 
           (match optionpos with 
              | None -> 
-		 lambda_name 
+		 lambda_name env
 		   (n,t,process_constr (i+1) c_0 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) rest)
+		      (applist(whd_beta_stack env sigma (lift 1 f) 
+				 [(Rel 1)])) rest)
              | Some(_,f_0) -> 
 		 let nF = lift (i+1+decF) f_0 in
 		 let arg = process_pos nF (lift 1 t) in 
-                 lambda_name 
+                 lambda_name env
 		   (n,t,process_constr (i+1) c_0 
-		      (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
+		      (applist(whd_beta_stack env sigma (lift 1 f) 
+				 [(Rel 1); arg])) 
 		      rest))
       | (DOPN(MutInd(_,tyi),_),largs) -> f
       | _ -> assert false
   in 
   process_constr 0 st f recargs 
 
-let mis_make_indrec sigma listdepkind mispec =
+let mis_make_indrec env sigma listdepkind mispec =
   let nparams = mis_nparams mispec in
   let recargsvec = mis_recargs mispec in
   let ntypes = mis_ntypes mispec in
   let mind_arity = mis_arity mispec in 
-  let (lnames, ckind) = splay_prod sigma mind_arity in
+  let (lnames, ckind) = splay_prod env sigma mind_arity in
   let kind = destSort ckind in
-  let lnamespar = lastn nparams lnames in
+  let lnamespar = list_lastn nparams lnames in
   let listdepkind = 
     if listdepkind = [] then 
       let dep = kind <> Prop Null in [(mispec,dep,kind)] 
@@ -244,7 +244,7 @@ let mis_make_indrec sigma listdepkind mispec =
       assign k = function 
 	| [] -> ()
         | (mispeci,dep,_)::rest -> 
-            (Array.set depPvec mispeci.tyi (Some(dep,Rel k));
+            (Array.set depPvec mispeci.mis_tyi (Some(dep,Rel k));
              assign (k-1) rest)
     in 
     assign nrec listdepkind  
@@ -253,30 +253,30 @@ let mis_make_indrec sigma listdepkind mispec =
     let makefix nbconstruct = 
       let rec mrec i ln ltyp ldef = function 
 	| (mispeci,dep,_)::rest -> 
-	    let tyi = mispeci.tyi in
-	    let mind = DOPN(MutInd (mispeci.sp,tyi),mispeci.args) in
+	    let tyi = mispeci.mis_tyi in
+	    let mind = DOPN(MutInd (mispeci.mis_sp,tyi),mispeci.mis_args) in
 	    let (_,lct) = mis_type_mconstructs mispeci in
 	    let nctyi = Array.length lct in (* nb constructeurs du type *) 
-	    let realar =  hnf_prod_appvect sigma "make_branch" 
+	    let realar =  hnf_prod_appvect env sigma "make_branch" 
 			    (mis_arity mispeci) 
 			    (rel_vect (nrec+nbconstruct) nparams) in
                (* arity in the contexte P1..Prec f1..f_nbconstruct *)
-	    let lnames,_ = splay_prod sigma realar in 
+	    let lnames,_ = splay_prod env sigma realar in 
 	    let nar = List.length lnames in 
 	    let decf = nar+nrec+nbconstruct+nrec in 
 	    let dect = nar+nrec+nbconstruct in
 	    let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
 	    let branches = 
-	      map3_vect 
-		(rec_branch_arg (sigma,rel_vect (decf+1) nparams,
-				 depPvec,nar+1))
+	      array_map3
+		(rec_branch_arg env sigma 
+		   (rel_vect (decf+1) nparams,depPvec,nar+1))
                 vecfi lct recargsvec.(tyi) in
 	    let j = (match depPvec.(tyi) with 
 		       | Some (_,Rel j) -> j 
 		       | _ -> assert false) in
 	    let deftyi = 
-	      it_lambda_name 
-		(lambda_create 
+	      it_lambda_name env
+		(lambda_create env
 		   (appvect (mind,(Array.append (rel_vect decf nparams)
 				     (rel_vect 0 nar))),
 		    mkMutCaseA (ci_of_mind mind)
@@ -284,8 +284,8 @@ let mis_make_indrec sigma listdepkind mispec =
 		(lift_context nrec lnames)
 	    in
 	    let typtyi = 
-	      it_prod_name 
-		(prod_create 
+	      it_prod_name env
+		(prod_create env
 		   (appvect (mind,(Array.append (rel_vect dect nparams)
 				     (rel_vect 0 nar))),
 		    (if dep then 
@@ -301,7 +301,7 @@ let mis_make_indrec sigma listdepkind mispec =
             let fixdef = Array.of_list (List.rev ldef) in 
             let makefixdef = 
               put_DLAMSV 
-		(tabulate_list (fun _ -> Name(id_of_string "F")) nrec) fixdef 
+		(list_tabulate (fun _ -> Name(id_of_string "F")) nrec) fixdef 
 	    in 
             let fixspec = Array.append fixtyi [|makefixdef|] in 
 	    DOPN(Fix(fixn,p),fixspec)
@@ -310,7 +310,7 @@ let mis_make_indrec sigma listdepkind mispec =
     in 
     let rec make_branch i = function 
       | (mispeci,dep,_)::rest -> 
-	  let tyi = mispeci.tyi in
+	  let tyi = mispeci.mis_tyi in
 	  let (lc,lct) = mis_type_mconstructs mispeci in 
 	  let rec onerec j = 
 	    if j = Array.length lc then 
@@ -321,7 +321,7 @@ let mis_make_indrec sigma listdepkind mispec =
 	      let recarg = recargsvec.(tyi).(j) in
 	      let vargs = rel_vect (nrec+i+j) nparams in
 	      let p_0 = 
-		type_rec_branch dep (sigma,vargs,depPvec,i+j) co t recarg
+		type_rec_branch dep env sigma (vargs,depPvec,i+j) co t recarg
 	      in 
 	      DOP2(Lambda,p_0,DLAM(Name (id_of_string "f"),onerec (j+1)))
 	  in onerec 0
@@ -329,37 +329,37 @@ let mis_make_indrec sigma listdepkind mispec =
 	  makefix i listdepkind
     in 
     let rec put_arity i = function 
-      | ((mispeci,dep,kinds)::rest) -> 
-	  let mind = DOPN(MutInd (mispeci.sp,mispeci.tyi),mispeci.args) in 
+      | (mispeci,dep,kinds)::rest -> 
+	  let mind = DOPN(MutInd (mispeci.mis_sp,mispeci.mis_tyi),
+			  mispeci.mis_args) in 
 	  let arity = mis_arity mispeci in 
 	  let ar =
-	    hnf_prod_appvect sigma "put_arity" arity (rel_vect i nparams)
+	    hnf_prod_appvect env sigma "put_arity" arity (rel_vect i nparams)
 	  in 
 	  let typP = 
 	    if dep then 
-	      make_arity_dep (DOP0(Sort kinds)) ar 
+	      make_arity_dep env sigma (DOP0(Sort kinds)) ar 
 		(appvect (mind,rel_vect i nparams))
             else 
-	      make_arity_nodep (DOP0(Sort kinds)) ar 
+	      make_arity_nodep env sigma (DOP0(Sort kinds)) ar 
 	  in 
 	  DOP2(Lambda,typP,DLAM(Name(id_of_string "P"),put_arity (i+1) rest))
       | [] -> 
 	  make_branch 0 listdepkind 
     in 
     let (mispeci,dep,kind) = List.nth listdepkind p in
-    if is_recursive (List.map (fun (mispec,_,_) -> mispec.tyi) listdepkind)
-      recargsvec.(mispeci.tyi) then 
-   	it_lambda_name (put_arity 0 listdepkind) lnamespar
+    if is_recursive (List.map (fun (mispec,_,_) -> mispec.mis_tyi) listdepkind)
+      recargsvec.(mispeci.mis_tyi) then 
+   	it_lambda_name env (put_arity 0 listdepkind) lnamespar
    else 
-     mis_make_case_com (Some dep) sigma mispeci kind 
+     mis_make_case_com (Some dep) env sigma mispeci kind 
   in 
-  tabulate_vect make_one_rec nrec
+  Array.init nrec make_one_rec
 
-let make_indrec sigma listdepkind mind =
-  let ity = minductype_spec sigma mind in
-  let (sp,tyi,largs) = destMutInd ity in
-  let mispec = mind_specif_of_mind ity in  
-  mis_make_indrec sigma listdepkind mispec 
+let make_indrec env sigma listdepkind mind =
+  let ity = minductype_spec env sigma mind in
+  let mispec = lookup_mind_specif ity env in  
+  mis_make_indrec env sigma listdepkind mispec 
     
 let change_sort_arity sort = 
   let rec drec = function 
@@ -383,67 +383,55 @@ let instanciate_indrec_scheme sort =
 let check_arities listdepkind = 
   List.iter 
     (function (mispeci,dep,kinds) -> 
-       let mip = mispeci.mip  in
-       if dep then 
-	 let kd = mis_kd mispeci in 
-	 if List.exists (sort_cmp CONV_X kinds) kd then 
-	   ()
-	 else 
-	   errorlabstrm "Bad Induction"
-	     [<'sTR "Dependent induction for type "; 
-	       print_id mip.mINDTYPENAME;
-	       'sTR " and sort "; pTERM (DOP0(Sort kinds)); 
-	       'sTR "is not allowed">]
-       else 
-	 let kn = mis_kn mispeci in 
-	 if List.exists (sort_cmp CONV_X kinds) kn then 
-	   ()
-         else 
-	   errorlabstrm "Bad Induction"
-	     [<'sTR "Non dependent induction for type "; 
-	       print_id mip.mINDTYPENAME;
-	       'sTR " and sort "; pTERM (DOP0(Sort kinds)); 
-	       'sTR "is not allowed">])
+       let mip = mispeci.mis_mip  in
+       let kelim = mis_kelim mispeci in
+       if not (List.exists (base_sort_cmp CONV kinds) kelim) then 
+	 errorlabstrm "Bad Induction"
+	   [<'sTR (if dep then "Dependent" else "Non dependend");
+	     'sTR " induction for type "; 
+	     print_id mip.mind_typename;
+	     'sTR " and sort "; print_sort kinds; 
+	     'sTR "is not allowed">])
     listdepkind
 
-let build_indrec sigma = function 
-  | ((mind,dep,s)::lrecspec) ->
-      let redind = minductype_spec sigma mind in 
+let build_indrec env sigma = function 
+  | (mind,dep,s)::lrecspec ->
+      let redind = minductype_spec env sigma mind in 
       let (sp,tyi,_) = destMutInd redind in 
       let listdepkind = 
-    	(mind_specif_of_mind redind, dep,s)::
+    	(lookup_mind_specif redind env, dep,s)::
     	(List.map (function (mind',dep',s') ->
-		     let redind' = minductype_spec sigma mind' in
+		     let redind' = minductype_spec env sigma mind' in
 		     let (sp',_,_) = destMutInd redind' in
 		     if sp=sp' then 
-		       (mind_specif_of_mind redind',dep',s') 
+		       (lookup_mind_specif redind' env,dep',s') 
 		     else 
 		       error 
 			 "Induction schemes concern mutually inductive types") 
 	   lrecspec) 
       in
       let _ = check_arities listdepkind in 
-      make_indrec sigma listdepkind mind
+      make_indrec env sigma listdepkind mind
   | _ -> assert false
 	
 
 (* In order to interpret the Match operator *)
 
 let type_mutind_rec env sigma ct pt p c = 
-  let (mI,largs as mind) = find_minductype sigma ct in
-  let mispec = mind_specif_of_mind mI in 
-  let recargs =  mis_recarg mispec in
-  if is_recursive [mispec.tyi] recargs then
-    let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in 
+  let (mI,largs as mind) = find_minductype env sigma ct in
+  let mispec = lookup_mind_specif mI env in 
+  let recargs = mis_recarg mispec in
+  if is_recursive [mispec.mis_tyi] recargs then
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) mind pt in 
     let ntypes = mis_nconstr mispec 
-    and tyi = mispec.tyi 
+    and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
     let depPvec = Array.create ntypes (None : (bool * constr) option) in 
-    let _ = Array.set depPvec mispec.tyi (Some(dep,p)) in 
-    let (pargs,realargs) = chop_list nparams largs in
+    let _ = Array.set depPvec mispec.mis_tyi (Some(dep,p)) in 
+    let (pargs,realargs) = list_chop nparams largs in
     let vargs = Array.of_list pargs in
     let (constrvec,typeconstrvec) = mis_type_mconstructs mispec in
-    let lft = map3_vect (type_rec_branch dep (sigma,vargs,depPvec,0)) 
+    let lft = array_map3 (type_rec_branch dep env sigma (vargs,depPvec,0)) 
                 constrvec typeconstrvec recargs in
     (mI, lft,
      if dep then applist(p,realargs@[c]) 
@@ -451,11 +439,11 @@ let type_mutind_rec env sigma ct pt p c =
   else 
     type_case_branches env sigma ct pt p c
 
-let is_mutind sigma ct =  
-  try let _ = find_minductype sigma ct in true with Induc -> false
+let is_mutind env sigma ct =  
+  try let _ = find_minductype env sigma ct in true with Induc -> false
 
-let type_rec_branches recursive sigma env ct pt p c = 
-  match whd_betadeltaiota_stack sigma ct [] with 
+let type_rec_branches recursive env sigma ct pt p c = 
+  match whd_betadeltaiota_stack env sigma ct [] with 
     | (DOPN(MutInd _,_),_) -> 
 	if recursive then 
 	  type_mutind_rec env sigma ct pt p c
@@ -468,7 +456,7 @@ let type_rec_branches recursive sigma env ct pt p c =
 
 let stacklamxtra recfun = 
   let rec lamrec sigma p_0 p_1 = match p_0,p_1 with 
-    | (stack, (DOP2(Lambda,DOP1(XTRA("COMMENT",[]),_),DLAM(_,c)) as t)) ->
+    | (stack, (DOP2(Lambda,DOP1(XTRA "COMMENT",_),DLAM(_,c)) as t)) ->
         recfun stack (substl sigma t)
     | ((h::t), (DOP2(Lambda,_,DLAM(_,c)))) -> lamrec (h::sigma) t c
     | (stack, t) -> recfun stack (substl sigma t)
@@ -477,55 +465,55 @@ let stacklamxtra recfun =
 
 let rec whrec x stack =
   match x with   
-    | DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t)) ->
+    | DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t)) ->
     	let t' = applist (whrec t (List.map (lift 1) stack)) in 
-	DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t')),[]
+	DOP2(Lambda,DOP1(XTRA "COMMENT",c),DLAM(name,t')),[]
     | DOP2(Lambda,c1,DLAM(name,c2)) ->
     	(match stack with
 	   | [] -> (DOP2(Lambda,c1,DLAM(name,whd_betaxtra c2)),[])
 	   | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2)
-    | DOPN(AppL,cl)      -> whrec (hd_vect cl) (app_tl_vect cl stack)
-    | DOP2(Cast,c,_)       ->  whrec c stack
+    | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
+    | DOP2(Cast,c,_) ->  whrec c stack
     | x -> x,stack
 
 and whd_betaxtra x = applist(whrec x [])
 
 let transform_rec env sigma cl (ct,pt) = 
-  let (mI,largs as mind) = find_minductype sigma ct in
+  let (mI,largs as mind) = find_minductype env sigma ct in
   let p = cl.(0)
   and c = cl.(1)
   and lf = Array.sub cl 2 ((Array.length cl) - 2) in
-  let mispec = mind_specif_of_mind mI in 
-  let recargs =  mis_recarg mispec in
+  let mispec = lookup_mind_specif mI env in 
+  let recargs = mis_recarg mispec in
   let expn = Array.length recargs in
   if Array.length lf <> expn then error_number_branches CCI env c ct expn;
-  if is_recursive [mispec.tyi] recargs then
-    let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in 
+  if is_recursive [mispec.mis_tyi] recargs then
+    let (dep,_) = find_case_dep_nparams env sigma (c,p) mind pt in 
     let ntypes = mis_nconstr mispec 
-    and tyi = mispec.tyi 
+    and tyi = mispec.mis_tyi 
     and nparams = mis_nparams mispec in
     let depFvec = Array.create ntypes (None : (bool * constr) option) in 
-    let _ = Array.set depFvec mispec.tyi (Some(dep,Rel 1)) in 
-    let (pargs,realargs) = chop_list nparams largs in
+    let _ = Array.set depFvec mispec.mis_tyi (Some(dep,Rel 1)) in 
+    let (pargs,realargs) = list_chop nparams largs in
     let vargs = Array.of_list pargs in
     let (_,typeconstrvec) = mis_type_mconstructs mispec in
     (* build now the fixpoint *)
     let realar =
-      hnf_prod_appvect sigma "make_branch" (mis_arity mispec) vargs in
-    let lnames,_ = splay_prod sigma realar in 
+      hnf_prod_appvect env sigma "make_branch" (mis_arity mispec) vargs in
+    let lnames,_ = splay_prod env sigma realar in 
     let nar = List.length lnames in
     let branches = 
-      map3_vect 
+      array_map3
 	(fun f t reca -> 
 	   whd_betaxtra
-             (rec_branch_arg
-                (sigma,(Array.map (lift (nar+2)) vargs),depFvec,nar+1)
+             (rec_branch_arg env sigma
+                ((Array.map (lift (nar+2)) vargs),depFvec,nar+1)
                 f t reca))
         (Array.map (lift (nar+2)) lf) typeconstrvec recargs 
     in 
     let deffix = 
-      it_lambda_name 
-	(lambda_create 
+      it_lambda_name env
+	(lambda_create env
 	   (appvect (mI,Array.append (Array.map (lift (nar+1)) vargs)
                        (rel_vect 0 nar)),
             mkMutCaseA (ci_of_mind mI) 
@@ -533,17 +521,20 @@ let transform_rec env sigma cl (ct,pt) =
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
-      whd_beta (applist (pop deffix,realargs@[c]))
+      whd_beta env sigma (applist (pop deffix,realargs@[c]))
     else
       let typPfix = 
-	it_prod_name  
-	  (prod_create (appvect (mI,(Array.append 
-				       (Array.map (lift nar) vargs)
-				       (rel_vect 0 nar))),
-			(if dep then applist (whd_beta_stack (lift (nar+1) p)
-                                                (rel_list 0 (nar+1)))
-			 else applist (whd_beta_stack (lift (nar+1) p) 
-                                         (rel_list 1 nar)))))
+	it_prod_name env
+	  (prod_create env
+	     (appvect (mI,(Array.append 
+			     (Array.map (lift nar) vargs)
+			     (rel_vect 0 nar))),
+	      (if dep then 
+		 applist (whd_beta_stack env sigma 
+			    (lift (nar+1) p) (rel_list 0 (nar+1)))
+	       else 
+		 applist (whd_beta_stack env sigma 
+			    (lift (nar+1) p) (rel_list 1 nar)))))
           lnames 
       in
       let fix = DOPN(Fix([|nar|],0),
@@ -556,9 +547,9 @@ let transform_rec env sigma cl (ct,pt) =
 
 (*** Building ML like case expressions without types ***)
 
-let concl_n sigma = 
+let concl_n env sigma = 
   let rec decrec m c = if m = 0 then c else 
-    match whd_betadeltaiota sigma c with
+    match whd_betadeltaiota env sigma c with
       | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
       | _                        -> failwith "Typing.concl_n"
   in 
@@ -572,16 +563,16 @@ let count_rec_arg j =
   in 
   crec 0
     
-let norec_branch_scheme sigma typc =
-  let rec crec typc = match whd_betadeltaiota sigma typc with 
+let norec_branch_scheme env sigma typc =
+  let rec crec typc = match whd_betadeltaiota env sigma typc with 
     | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t))
     | _ -> mkExistential
   in 
   crec typc
 
-let rec_branch_scheme sigma j typc recargs = 
+let rec_branch_scheme env sigma j typc recargs = 
   let rec crec (typc,recargs) = 
-    match whd_betadeltaiota sigma typc, recargs with 
+    match whd_betadeltaiota env sigma typc, recargs with 
       | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> 
           DOP2(Prod,c,
 	       match ra with 
@@ -596,26 +587,27 @@ let rec_branch_scheme sigma j typc recargs =
   in 
   crec (typc,recargs) 
     
-let branch_scheme sigma isrec i mind = 
-  let typc =  type_inst_construct sigma i mind in 
+let branch_scheme env sigma isrec i mind = 
+  let typc = type_inst_construct env sigma i mind in 
   if isrec then
-    let (mI,_) = find_mrectype sigma mind in
+    let (mI,_) = find_mrectype env sigma mind in
     let (_,j,_) = destMutInd mI in
-    let mispec = mind_specif_of_mind mI in 
+    let mispec = lookup_mind_specif mI env in 
     let recarg = (mis_recarg mispec).(i-1) in
-    rec_branch_scheme sigma j typc recarg
+    rec_branch_scheme env sigma j typc recarg
   else 
-    norec_branch_scheme sigma typc
+    norec_branch_scheme env sigma typc
 
 (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
  * K parameters. Then then build_notdep builds the predicate
  * [a_bar:A'_bar](lift k pred) 
  * where A'_bar = A_bar[p_bar <- globargs] *)
 
-let build_notdep_pred mispec nparams globargs pred =
+let build_notdep_pred env sigma mispec nparams globargs pred =
   let arity = mis_arity mispec in
   let lamarity = to_lambda nparams arity in
-  let inst_arity = whd_beta (appvect (lamarity,Array.of_list globargs)) in
+  let inst_arity = 
+    whd_beta env sigma (appvect (lamarity,Array.of_list globargs)) in
   let k = nb_prod inst_arity in
   let env,_,npredlist = push_and_liftl k [] inst_arity [insert_lifted pred] in
   let npred = (match npredlist with [npred] -> npred 
@@ -624,20 +616,20 @@ let build_notdep_pred mispec nparams globargs pred =
   in 
   finalpred
 
-let pred_case_ml_fail sigma isrec ct (i,ft) =
+let pred_case_ml_fail env sigma isrec ct (i,ft) =
   try 
-    let (mI,largs) = find_mrectype sigma ct in
+    let (mI,largs) = find_mrectype env sigma ct in
     let (_,j,_) = destMutInd mI in
-    let mispec = mind_specif_of_mind mI in
+    let mispec = lookup_mind_specif mI env in
     let nparams = mis_nparams mispec in
-    let (globargs,la) = chop_list nparams largs in
+    let (globargs,la) = list_chop nparams largs in
     let pred = 
       let recargs = (mis_recarg mispec) in
       assert (Array.length recargs <> 0);
       let recargi = recargs.(i-1) in
       let nbrec = if isrec then count_rec_arg j recargi else 0 in
       let nb_arg = List.length (recargs.(i-1)) + nbrec in
-      let pred = concl_n sigma nb_arg ft in
+      let pred = concl_n env sigma nb_arg ft in
       if noccur_bet 1 nb_arg pred then 
 	lift (-nb_arg) pred
       else 
@@ -646,25 +638,25 @@ let pred_case_ml_fail sigma isrec ct (i,ft) =
     if la = [] then 
       pred
     else (* we try with [_:T1]..[_:Tn](lift n pred) *)
-      build_notdep_pred mispec nparams globargs pred  
+      build_notdep_pred env sigma mispec nparams globargs pred  
   with Induc -> 
     failwith "Inductive"
 
 let pred_case_ml env sigma isrec (c,ct) lf (i,ft) = 
   try 
-    pred_case_ml_fail sigma isrec ct (i,ft)
+    pred_case_ml_fail env sigma isrec ct (i,ft)
   with Failure mes -> 
-    error_ml_case mes env c ct lf.(i-1) ft
+    error_ml_case CCI env mes c ct lf.(i-1) ft
 
 (* similar to pred_case_ml but does not expect the list lf of braches *)
 let pred_case_ml_onebranch env sigma isrec (c,ct) (i,f,ft) = 
   try 
-    pred_case_ml_fail sigma isrec ct (i,ft)
+    pred_case_ml_fail env sigma isrec ct (i,ft)
   with Failure mes -> 
-    error_ml_case mes env c ct f ft
+    error_ml_case CCI env mes c ct f ft
       
 let make_case_ml isrec pred c ci lf = 
   if isrec then 
-    DOPN(XTRA("REC",[]),Array.append [|pred;c|] lf)
+    DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
   else 
     mkMutCaseA ci pred c lf
diff --git a/library/indrec.mli b/library/indrec.mli
index 408c97e39f..04cd875729 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -11,19 +11,20 @@ open Evd
 
 (* Eliminations. *)
 
-val make_case_dep : 'c evar_map -> constr -> sorts -> constr
-val make_case_nodep : 'c evar_map -> constr -> sorts -> constr
-val make_case_gen : 'c evar_map -> constr -> sorts -> constr
+val make_case_dep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_nodep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_gen : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
 
-val make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list 
-  -> constr -> constr array
+val make_indrec : unsafe_env -> 'a evar_map -> 
+  (mind_specif * bool * sorts) list -> constr -> constr array
 
-val mis_make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list 
-  -> mind_specif -> constr array
+val mis_make_indrec : unsafe_env -> 'a evar_map -> 
+  (mind_specif * bool * sorts) list -> mind_specif -> constr array
 
 val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 
-val build_indrec : 'c evar_map -> (constr * bool * sorts) list -> constr array
+val build_indrec : 
+  unsafe_env -> 'a evar_map -> (constr * bool * sorts) list -> constr array
 
 val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr 
   -> constr -> constr -> constr -> constr * constr array * constr
@@ -31,9 +32,10 @@ val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr
 val transform_rec : unsafe_env -> 'c evar_map -> (constr array) 
   -> (constr * constr) -> constr
 
-val is_mutind : 'c evar_map -> constr -> bool 
+val is_mutind : unsafe_env -> 'a evar_map -> constr -> bool 
 
-val branch_scheme : 'c evar_map -> bool -> int -> constr -> constr
+val branch_scheme : 
+  unsafe_env -> 'a evar_map -> bool -> int -> constr -> constr
 
 val pred_case_ml : unsafe_env -> 'c evar_map -> bool -> (constr * constr) 
   ->  constr array -> (int*constr)  ->constr
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 59f9cdf69f..2b2f9b8b44 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -32,4 +32,6 @@ type refiner_error =
   | NotWellTyped of constr
   | BadTacticArgs of string * tactic_arg list
 
+exception RefinerError of refiner_error
+
 val error_cannot_unify : path_kind -> constr * constr -> 'a
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
new file mode 100644
index 0000000000..07ef757a56
--- /dev/null
+++ b/tactics/hiddentac.ml
@@ -0,0 +1,40 @@
+
+(* $Id$ *)
+
+open Term
+open Proof_trees
+open Tacmach
+open Tacentries
+
+(* These tactics go through the interpreter. They left a trace in the proof
+   tree when they are called. *)
+
+let h_clear ids         = v_clear  [(Clause ids)]
+let h_move dep id1 id2  = 
+ (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
+let h_contradiction     = v_contradiction []
+let h_reflexivity       = v_reflexivity   []
+let h_symmetry          = v_symmetry      []
+let h_assumption        = v_assumption    []
+let h_absurd c          = v_absurd [(Constr c)]
+let h_exact  c          = v_exact  [(Constr c)]
+let h_one_constructor i = v_constructor [(Integer i)]
+let h_any_constructor   = v_constructor []
+let h_transitivity c    = v_transitivity [(Constr c)]
+let h_simplest_left     = v_left [(Cbindings [])]
+let h_simplest_right    = v_right [(Cbindings [])]
+let h_split     c       = v_split [(Constr c);(Cbindings [])]
+let h_apply c s         = v_apply  [(Constr c);(Cbindings s)]
+let h_simplest_apply c  = v_apply  [(Constr c);(Cbindings [])]
+let h_cut      c        = v_cut [(Constr c)]
+let h_simplest_elim c   = v_elim [(Constr c);(Cbindings [])]
+let h_elimType     c    = v_elimType [(Constr c)]
+let h_inductionInt  i   = v_induction[(Integer i)]
+let h_inductionId   id  = v_induction[(Identifier id)]
+let h_simplest_case   c = v_case [(Constr c);(Cbindings [])]
+let h_caseType        c = v_caseType [(Constr c)]
+let h_destructInt  i    = v_destruct [(Integer i)]
+let h_destructId   id   = v_destruct [(Identifier id)]
+
+
+
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
new file mode 100644
index 0000000000..1d9b25757a
--- /dev/null
+++ b/tactics/hiddentac.mli
@@ -0,0 +1,37 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Proof_trees
+open Tacmach
+open Tacentries
+(*i*)
+
+val h_clear           : identifier list -> tactic
+val h_move            : bool -> identifier -> identifier -> tactic
+val h_contradiction   : tactic
+val h_reflexivity     : tactic
+val h_symmetry        : tactic
+val h_assumption      : tactic
+val h_absurd          : constr -> tactic
+val h_exact           : constr -> tactic
+val h_one_constructor : int -> tactic
+val h_any_constructor : tactic
+val h_transitivity    : constr -> tactic
+val h_simplest_left   : tactic
+val h_simplest_right  : tactic
+val h_split           : constr -> tactic
+val h_apply           : constr -> constr substitution -> tactic
+val h_simplest_apply  : constr -> tactic 
+val h_cut             : constr -> tactic 
+val h_simplest_elim   : constr -> tactic
+val h_elimType        : constr -> tactic
+val h_simplest_case   : constr -> tactic
+val h_caseType        : constr -> tactic
+val h_inductionInt    : int -> tactic 
+val h_inductionId     : identifier -> tactic 
+val h_destructInt     : int -> tactic
+val h_destructId      : identifier -> tactic
+
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
new file mode 100644
index 0000000000..a91c5f4fc2
--- /dev/null
+++ b/tactics/tacentries.ml
@@ -0,0 +1,45 @@
+
+(* $Id$ *)
+
+open Proof_trees
+open Tacmach
+open Tactics
+open Tacticals
+
+let v_absurd        = hide_tactic "Absurd"        dyn_absurd
+let v_contradiction = hide_tactic "Contradiction" dyn_contradiction
+let v_reflexivity   = hide_tactic "Reflexivity"   dyn_reflexivity
+let v_symmetry      = hide_tactic "Symmetry"      dyn_symmetry
+let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
+let v_intro         = hide_tactic "Intro"         dyn_intro
+let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
+let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
+let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
+let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL
+let v_assumption    = hide_tactic "Assumption"    dyn_assumption
+let v_exact         = hide_tactic "Exact"         dyn_exact
+let v_reduce        = hide_tactic "Reduce"        dyn_reduce
+let v_change        = hide_tactic "Change"        dyn_change
+let v_constructor   = hide_tactic "Constructor"   dyn_constructor
+let v_left          = hide_tactic "Left"          dyn_left
+let v_right         = hide_tactic "Right"         dyn_right
+let v_split         = hide_tactic "Split"         dyn_split
+let v_clear         = hide_tactic "Clear"         dyn_clear
+let v_move          = hide_tactic "Move"          dyn_move
+let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
+let v_apply         = hide_tactic "Apply"         dyn_apply
+let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
+let v_cut           = hide_tactic "Cut"           dyn_cut
+let v_lettac        = hide_tactic "LetTac"        dyn_lettac
+let v_generalize    = hide_tactic "Generalize"    dyn_generalize
+let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
+let v_specialize    = hide_tactic "Specialize"    dyn_new_hyp
+let v_elim          = hide_tactic "Elim"          dyn_elim
+let v_elimType      = hide_tactic "ElimType"      dyn_elim_type
+let v_induction     = hide_tactic "Induction"     dyn_induct
+let v_case          = hide_tactic "Case"          dyn_case
+let v_caseType      = hide_tactic "CaseType"      dyn_case_type
+let v_destruct      = hide_tactic "Destruct"      dyn_destruct
+let v_fix           = hide_tactic "Fix"           dyn_mutual_fix
+let v_cofix         = hide_tactic "Cofix"         dyn_mutual_cofix
+
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
new file mode 100644
index 0000000000..ed19fd8d82
--- /dev/null
+++ b/tactics/tacentries.mli
@@ -0,0 +1,41 @@
+
+(* $Id$ *)
+
+(*i*)
+open Proof_trees
+open Tacmach
+(*i*)
+
+val v_absurd        : tactic_arg list -> tactic
+val v_contradiction : tactic_arg list -> tactic
+val v_reflexivity   : tactic_arg list -> tactic
+val v_symmetry      : tactic_arg list -> tactic
+val v_transitivity  : tactic_arg list -> tactic
+val v_intro         : tactic_arg list -> tactic
+val v_introsUntil   : tactic_arg list -> tactic
+val v_tclIDTAC      : tactic_arg list -> tactic
+val v_assumption    : tactic_arg list -> tactic
+val v_exact         : tactic_arg list -> tactic
+val v_reduce        : tactic_arg list -> tactic
+val v_constructor   : tactic_arg list -> tactic
+val v_left          : tactic_arg list -> tactic
+val v_right         : tactic_arg list -> tactic
+val v_split         : tactic_arg list -> tactic
+val v_clear         : tactic_arg list -> tactic
+val v_move          : tactic_arg list -> tactic
+val v_move_dep      : tactic_arg list -> tactic
+val v_apply         : tactic_arg list -> tactic
+val v_cutAndResolve : tactic_arg list -> tactic
+val v_cut           : tactic_arg list -> tactic
+val v_lettac        : tactic_arg list -> tactic
+val v_generalize    : tactic_arg list -> tactic
+val v_generalize_dep : tactic_arg list -> tactic
+val v_specialize    : tactic_arg list -> tactic
+val v_elim          : tactic_arg list -> tactic
+val v_elimType      : tactic_arg list -> tactic
+val v_induction     : tactic_arg list -> tactic
+val v_case          : tactic_arg list -> tactic
+val v_caseType      : tactic_arg list -> tactic
+val v_destruct      : tactic_arg list -> tactic
+val v_fix           : tactic_arg list -> tactic
+val v_cofix         : tactic_arg list -> tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 49c384df4a..bd66561dd8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -374,7 +374,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
   let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
-  let elim  = Indrec.make_case_gen sigma ity sort in  
+  let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -383,7 +383,7 @@ let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
-  let elim  = Indrec.make_case_nodep sigma ity sort in  
+  let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
   general_elim_then_using 
     elim case_sign tac predicate (indbindings,elimbindings) c gl
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index d39d347282..07c35ab321 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -186,6 +186,33 @@ let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
      'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
      'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
 
+let explain_not_inductive k ctx c =
+  let pc = P.pr_term k ctx c in
+  [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
+     'sTR "is not an inductive definition" >]
+
+let explain_ml_case k ctx mes c ct br brt =
+  let pc = P.pr_term k ctx c in
+  let pct = P.pr_term k ctx ct in
+  let expln =
+    match mes with
+      | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
+      | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
+      | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
+      | "Decomp" ->
+          let plf = P.pr_term k ctx br in
+          let pft = P.pr_term k ctx brt in
+          [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
+             'wS 1; 'cUT;
+             'sTR "does not correspond to the inductive definition" >]
+      | "Dependent" ->
+          [< 'sTR "ML case not allowed for a dependent case elimination">]
+      | _ -> [<>]
+  in
+  hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
+           'sTR "of type";  'wS 1; pct; 'wS 1; 'cUT; 
+           'sTR "which is an inductive predicate."; 'fNL; expln >]
+
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n
@@ -215,6 +242,10 @@ let explain_type_error k ctx = function
       explain_ill_formed_rec_body k ctx i lna vdefj vargs
   | IllTypedRecBody (i, lna, vdefj, vargs) ->
       explain_ill_typed_rec_body k ctx i lna vdefj vargs
+  | NotInductive c ->
+      explain_not_inductive k ctx c
+  | MLCase (mes,c,ct,br,brt) ->
+      explain_ml_case k ctx mes c ct br brt
 
 let explain_refiner_bad_type k ctx arg ty conclty =
   errorlabstrm "Logic.conv_leq_goal"