Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations

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

33 files changed, 1925 insertions, 161 deletions

diff --git a/.depend b/.depend
index 838153f837..08d6753751 100644
--- a/.depend
+++ b/.depend
@@ -80,8 +80,13 @@ proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
 proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/term.cmi 
 proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
+tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+    lib/util.cmi 
 tactics/btermdn.cmi: kernel/generic.cmi kernel/term.cmi 
 tactics/dn.cmi: lib/tlm.cmi 
+tactics/elim.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi kernel/term.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 \
@@ -234,16 +239,16 @@ lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
 lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
 lib/util.cmo: lib/pp.cmi lib/util.cmi 
 lib/util.cmx: lib/pp.cmx lib/util.cmi 
-library/declare.cmo: kernel/constant.cmi kernel/generic.cmi \
-    library/global.cmi library/impargs.cmi kernel/inductive.cmi \
-    library/lib.cmi library/libobject.cmi kernel/names.cmi \
-    library/nametab.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
-    library/declare.cmi 
-library/declare.cmx: kernel/constant.cmx kernel/generic.cmx \
-    library/global.cmx library/impargs.cmx kernel/inductive.cmx \
-    library/lib.cmx library/libobject.cmx kernel/names.cmx \
-    library/nametab.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
-    library/declare.cmi 
+library/declare.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi library/impargs.cmi library/indrec.cmi \
+    kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
+    kernel/names.cmi library/nametab.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi library/declare.cmi 
+library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx library/impargs.cmx library/indrec.cmx \
+    kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
+    kernel/names.cmx library/nametab.cmx kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi 
 library/global.cmo: kernel/generic.cmi kernel/inductive.cmi \
     kernel/instantiate.cmi kernel/sign.cmi library/summary.cmi \
     kernel/term.cmi kernel/typing.cmi lib/util.cmi library/global.cmi 
@@ -400,12 +405,52 @@ proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
 proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
     kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi 
+tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \
+    tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
+    tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi kernel/names.cmi \
+    tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \
+    proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi tactics/auto.cmi 
+tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \
+    tactics/dhyp.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
+    tactics/hiddentac.cmx kernel/inductive.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx kernel/names.cmx \
+    tactics/pattern.cmx proofs/pfedit.cmi lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \
+    proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmi tactics/auto.cmi 
 tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \
     tactics/btermdn.cmi 
 tactics/btermdn.cmx: tactics/dn.cmx kernel/term.cmx tactics/termdn.cmx \
     tactics/btermdn.cmi 
+tactics/dhyp.cmo: parsing/ast.cmi proofs/clenv.cmi kernel/generic.cmi \
+    toplevel/himsg.cmi library/lib.cmi library/libobject.cmi \
+    library/library.cmi kernel/names.cmi tactics/nbtermdn.cmi \
+    tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi library/summary.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi tactics/dhyp.cmi 
+tactics/dhyp.cmx: parsing/ast.cmx proofs/clenv.cmx kernel/generic.cmx \
+    toplevel/himsg.cmx library/lib.cmx library/libobject.cmx \
+    library/library.cmx kernel/names.cmx tactics/nbtermdn.cmx \
+    tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx library/summary.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmi tactics/dhyp.cmi 
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
+tactics/elim.cmo: proofs/clenv.cmi kernel/generic.cmi tactics/hiddentac.cmi \
+    kernel/names.cmi tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi tactics/elim.cmi 
+tactics/elim.cmx: proofs/clenv.cmx kernel/generic.cmx tactics/hiddentac.cmx \
+    kernel/names.cmx tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx tactics/elim.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 \
diff --git a/Makefile b/Makefile
index 8791b0c453..a710917ea7 100644
--- a/Makefile
+++ b/Makefile
@@ -56,8 +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/tactics.cmo \
-        tactics/tacentries.cmo tactics/hiddentac.cmo
+	tactics/wcclausenv.cmo tactics/tacticals.cmo \
+        tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
 
 PRETYPING=pretyping/astterm.cmo
 
diff --git a/dev/TODO b/dev/TODO
index 6b35783a25..356f1e5b60 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,14 +1,9 @@
 
- o Declare
-     - declare_eliminations
-
  o Discharge
      - conserver les constantes dans leur section de définition
        et redéfinir des constantes déchargées à la sortie
 
  o Variables existentielles
-     - traiter le constructeur Evar dans les fonctions de réductions
-       (parallèlement à Const)
      - unifier Meta et Evar
 
  o Lib
@@ -29,7 +24,8 @@
      - utiliser DOPL plutôt que DOPN (sauf pour Case)
      - batch mode => pas de undo, ni de reset
      - conversion : déplier la constante la plus récente
-     - un cache pour type_of_const, type_of_inductive, type_of_constructor
+     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
+       lookup_mind_specif
 
  o Lexer
      à compléter
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f6c27a8be6..6dd6c21774 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -143,7 +143,7 @@ let const_value_cache info c =
   try  
     Some (Hashtbl.find info.i_tab c)
   with Not_found ->
-    match const_abst_opt_value info.i_env c with
+    match const_abst_opt_value info.i_env info.i_evc c with
       | Some body ->
           let v = info.i_repr info body in
           Hashtbl.add info.i_tab c v;
@@ -349,7 +349,7 @@ let rec norm_head info env t stack =
                     reduce_const_body
                       (cbv_norm_more info) (shift_value n v) stack
                 | Inr n -> (VAL(0, Rel n), stack))
-  | DOPN ((Const _ | Abst _) as op, vars)
+  | DOPN ((Const _ | Evar _ | Abst _) as op, vars)
                   when red_allowed info.i_flags stack (DELTA op) ->
       let normt = DOPN(op, Array.map (cbv_norm_term info env) vars) in
       (match const_value_cache info normt with
@@ -751,7 +751,7 @@ and whnf_frterm info ft =
           { norm = uf.norm; term = FLIFT(k, uf) }
       | FOP2 (Cast,f,_) -> whnf_frterm info f  (* remove outer casts *)
       | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl)
-      | FOPN ((Const _ | Abst _) as op,vars) ->
+      | FOPN ((Const _ | Evar _ | Abst _) as op,vars) ->
 	  if red_under info.i_flags (DELTA op) then
             let cst = DOPN(op, Array.map term_of_freeze vars) in
             (match const_value_cache info cst with
@@ -818,7 +818,7 @@ and whnf_term info env t =
     | DOP2 (Cast,ct,c) -> whnf_term info env ct    (* remove outer casts *)
     | DOP2 (op,a,b) -> (* Lambda Prod *)
       	{ norm = false; term = FOP2 (op, freeze env a, freeze env b) }
-    | DOPN ((AppL | Const _ | Abst _ | MutCase _) as op, ve) ->
+    | DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) ->
       	whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) }
     | DOPN ((MutInd _ | MutConstruct _) as op,v) ->
       	{ norm = (v=[||]); term = FOPN (op, freeze_vect env v) }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a983a67597..f715e985aa 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -199,9 +199,6 @@ let defined_constant env = function
       Constant.is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
-(* A const is opaque if it is a non-defined existential or
-   a non-existential opaque constant *)
-
 let opaque_constant env = function
   | DOPN (Const sp, _) -> 
       Constant.is_opaque (lookup_constant sp env)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0154aa7a96..60139def2e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -49,6 +49,7 @@ let mis_recargs mis =
   Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
 let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
+let mis_consnames mis = mis.mis_mip.mind_consnames
 
 let is_recursive listind = 
   let rec one_is_rec rvec = 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index ceb8fa0deb..8140d949d7 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -58,6 +58,7 @@ 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 mis_consnames : mind_specif -> identifier array
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 07c5525263..819dfcf841 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -52,14 +52,6 @@ let constant_value env k =
   else 
     failwith "opaque"
 
-let const_abst_opt_value env c =
-  match c with
-    | DOPN(Const sp,_) ->
-	if evaluable_constant env c then Some (constant_value env c) else None
-    | DOPN(Abst sp,_) ->
-	if evaluable_abst env c then Some (abst_value env c) else None
-    | _ -> invalid_arg "const_abst_opt_value"
-
 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)
@@ -102,6 +94,19 @@ let existential_value sigma c =
     | Evar_empty ->
 	anomaly "a defined existential with no body"
 
+let const_abst_opt_value env sigma c =
+  match c with
+    | DOPN(Const sp,_) ->
+	if evaluable_constant env c then Some (constant_value env c) else None
+    | DOPN(Evar ev,_) ->
+	if Evd.is_defined sigma ev then 
+	  Some (existential_value sigma c) 
+	else 
+	  None
+    | DOPN(Abst sp,_) ->
+	if evaluable_abst env c then Some (abst_value env c) else None
+    | _ -> invalid_arg "const_abst_opt_value"
+
 let mis_arity' mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index ba5a072a1e..3764948843 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -22,7 +22,7 @@ val constant_type : unsafe_env -> constr -> typed_type
 val existential_value : 'a evar_map -> constr -> constr
 val existential_type : 'a evar_map -> constr -> constr
 
-val const_abst_opt_value : unsafe_env -> constr -> constr option
+val const_abst_opt_value : unsafe_env -> 'a evar_map -> constr -> constr option
 
 val mis_arity : mind_specif -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d4557efc6..bc4021fbf9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -100,93 +100,31 @@ let red_product env sigma c =
     match x with
       | DOPN(AppL,cl) -> 
 	  DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
-      | DOPN(Const _,_) when evaluable_constant env x -> constant_value env x
-      | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x 
+      | DOPN(Const _,_) when evaluable_constant env x -> 
+	  constant_value env x
+      | DOPN(Evar ev,_) when Evd.is_defined sigma ev -> 
+	  existential_value sigma x
+      | DOPN(Abst _,_) when evaluable_abst env x -> 
+	  abst_value env x 
       | DOP2(Cast,c,_) -> redrec c
       | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))  
       | _ -> error "Term not reducible"
   in 
   nf_betaiota env sigma (redrec c)
 
-
-(* Substitute only a list of locations locs, the empty list is interpreted
-   as substitute all, if 0 is in the list then no substitution is done 
-   the list may contain only negative occurrences that will not be substituted *)
-(* Aurait sa place dans term.ml mais term.ml ne connait pas printer.ml *)
-let subst_term_occ locs c t = 
-  let rec substcheck except k occ c t =
-    if except or List.exists (function u -> u>=occ) locs then
-      substrec except k occ c t
-    else 
-      (occ,t)
-  and substrec except k occ c t =
-    if eq_constr t c then
-      if except then 
-	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
-      else 
-	if List.mem occ locs then (occ+1,Rel(k)) else  (occ+1,t)
-    else 
-      match t with
-	| DOPN(Const sp,tl) -> occ,t
-	|  DOPN(MutConstruct _,tl) -> occ,t
-	|  DOPN(MutInd _,tl) -> occ,t
-	|  DOPN(i,cl) -> 
-	     let (occ',cl') =   
-               Array.fold_left 
-		 (fun (nocc',lfd) f ->
-		    let (nocc'',f') = substcheck except k nocc' c f in
-                    (nocc'',f'::lfd)) 
-		 (occ,[]) cl
-             in 
-	     (occ',DOPN(i,Array.of_list (List.rev cl')))
-	|  DOP2(i,t1,t2) -> 
-	     let (nocc1,t1')=substrec except k occ c t1 in
-             let (nocc2,t2')=substcheck except k nocc1 c t2 in
-             nocc2,DOP2(i,t1',t2')
-	|  DOP1(i,t) -> 
-	     let (nocc,t')= substrec except k occ c t in
-	     nocc,DOP1(i,t')
-	|  DLAM(n,t) -> 
-	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
-             (occ',DLAM(n,t'))
-	|  DLAMV(n,cl) -> 
-	     let (occ',cl') =   
-               Array.fold_left 
-		 (fun (nocc',lfd) f ->
-		    let (nocc'',f') = 
-		      substcheck except (k+1) nocc' (lift 1 c) f
-                    in (nocc'',f'::lfd)) 
-		 (occ,[]) cl
-             in 
-	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
-	|  _ -> occ,t
-  in 
-  if locs = [] then 
-    subst_term c t
-  else if List.mem 0 locs then 
-    t
-  else 
-    let except = List.for_all (fun n -> n<0) locs in
-    let (nbocc,t') = substcheck except 1 1 c t in
-    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
-      failwith "subst_term_occ: too few occurences" 
-    else 
-      t'
-
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match c with
     | DOPN(Const sp,_) ->
-        if path_of_const c = name then
+        if sp = name then
           if List.hd ol = n then
             if evaluable_constant env c then 
-	      ((n+1),(List.tl ol), constant_value env c)
+	      (n+1, List.tl ol, constant_value env c)
             else
               errorlabstrm "substlin"
-                [< 'sTR(string_of_path sp);
-                   'sTR " is not a defined constant" >]
+                [< print_sp sp; 'sTR " is not a defined constant" >]
           else 
 	    ((n+1),ol,c)
         else 
@@ -195,13 +133,13 @@ let rec substlin env name n ol c =
     | DOPN(Abst _,_) ->
         if path_of_abst c = name then
           if List.hd ol = n then 
-	    ((n+1),(List.tl ol), abst_value env c)
+	    (n+1, List.tl ol, abst_value env c)
           else 
-	    ((n+1),ol,c)
+	    (n+1,ol,c)
         else 
 	  (n,ol,c)
 
-(* INEFFICIENT: OPTIMIZE *)
+    (* INEFFICIENT: OPTIMIZE *)
     | DOPN(AppL,tl) ->
         let c1 = array_hd tl and cl = array_tl tl in
         Array.fold_left 
@@ -394,6 +332,11 @@ let whd_delta_stack env sigma =
             whrec (constant_value env c) l
 	  else 
 	    x,l
+      | DOPN(Evar ev,_) as c ->
+	  if Evd.is_defined sigma ev then
+            whrec (existential_value sigma c) l
+	  else 
+	    x,l
       | (DOPN(Abst _,_)) as c ->
 	  if evaluable_abst env c then
             whrec (abst_value env c) l
@@ -416,6 +359,11 @@ let whd_betadelta_stack env sigma =
 	    whrec (constant_value env x) l
           else 
 	    (x,l)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then 
 	    whrec (abst_value env x) l
@@ -442,6 +390,11 @@ let whd_betadeltat_stack env sigma =
 	    whrec (constant_value env x) l
           else 
 	    (x,l)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
           if translucent_abst env x then 
 	    whrec (abst_value env x) l
@@ -467,6 +420,11 @@ let whd_betadeltaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then
 	    whrec (abst_value env x) stack
@@ -611,6 +569,11 @@ let whd_betadeltatiota_stack env sigma =
             whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if translucent_abst env x then
 	    whrec (abst_value env x) stack
@@ -648,6 +611,11 @@ let whd_betadeltaiota_stack env sigma =
 	    bdi_rec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    bdi_rec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then 
 	    bdi_rec (abst_value env x) stack 
@@ -686,6 +654,11 @@ let whd_betadeltaiotaeta_stack env sigma =
 	    whrec (constant_value env x) stack
           else 
 	    (x,stack)
+      | DOPN(Evar ev,_) ->
+          if Evd.is_defined sigma ev then 
+	    whrec (existential_value sigma x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
           if evaluable_abst env x then
 	    whrec (abst_value env x) stack
@@ -815,18 +788,19 @@ and eqappr cv_pb infos appr1 appr2 =
 	  (reloc_rel n el1 = reloc_rel m el2)
           (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
-    | (FOP0(Meta(n)), FOP0(Meta(m))) ->
+    | (FOP0(Meta n), FOP0(Meta m)) ->
         bool_and_convert (n=m) 
 	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
-    (* 2 constants or 2 abstractions *)
+    (* 2 constants, 2 existentials or 2 abstractions *)
     | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) ->
 	convert_or
 	  (* try first intensional equality *)
 	  (bool_and_convert (sp1 == sp2 or sp1 = sp2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Const sp2) al2 with
              | Some def2 -> 
@@ -836,13 +810,31 @@ and eqappr cv_pb infos appr1 appr2 =
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
 			  | None -> fun _ -> raise NotConvertible))
 
+    | (FOPN(Evar ev1,al1), FOPN(Evar ev2,al2)) ->
+	convert_or
+	  (* try first intensional equality *)
+	  (bool_and_convert (ev1 == ev2)
+	     (convert_and
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
+          (* else expand the second occurrence (arbitrary heuristic) *)
+          (match search_frozen_cst infos (Evar ev2) al2 with
+             | Some def2 -> 
+		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
+             | None -> (match search_frozen_cst infos (Evar ev1) al1 with
+                          | Some def1 -> eqappr cv_pb infos
+				(lft1, fhnf_apply infos n1 def1 v1) appr2
+			  | None -> fun _ -> raise NotConvertible))
+
     | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) ->
 	convert_or
 	  (* try first intensional equality *)
           (bool_and_convert  (sp1 = sp2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		   v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Abst sp2) al2 with
              | Some def2 -> 
@@ -852,14 +844,14 @@ and eqappr cv_pb infos appr1 appr2 =
 				(lft1, fhnf_apply infos n1 def1 v1) appr2
 			  | None -> fun _ -> raise NotConvertible))
 
-    (* only one constant or abstraction *)
-    | (FOPN((Const _ | Abst _) as op,al1), _)      ->
+    (* only one constant, existential or abstraction *)
+    | (FOPN((Const _ | Evar _ | Abst _) as op,al1), _)      ->
         (match search_frozen_cst infos op al1 with
            | Some def1 -> 
 	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
            | None -> fun _ -> raise NotConvertible)
 
-    | (_, FOPN((Const _ | Abst _) as op,al2))      ->
+    | (_, FOPN((Const _ | Evar _ | Abst _) as op,al2))      ->
         (match search_frozen_cst infos op al2 with
            | Some def2 -> 
 	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 1ff259e01a..67ad99f55a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -122,7 +122,6 @@ val unfoldn :
   (int list * section_path) list -> 'a reduction_function
 val fold_one_com : constr -> 'a reduction_function
 val fold_commands : constr list -> 'a reduction_function
-val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 543c41baa8..72d6cfbd2e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1139,6 +1139,71 @@ let rec subst_meta bl c =
     | DOP2(op,c'1, c'2) -> DOP2(op, subst_meta bl c'1, subst_meta bl c'2)
     | DOPN(op, c') -> DOPN(op, Array.map (subst_meta bl) c')
     | _ -> c
+
+(* Substitute only a list of locations locs, the empty list is
+   interpreted as substitute all, if 0 is in the list then no
+   substitution is done the list may contain only negative occurrences
+   that will not be substituted. *)
+
+let subst_term_occ locs c t = 
+  let rec substcheck except k occ c t =
+    if except or List.exists (function u -> u>=occ) locs then
+      substrec except k occ c t
+    else 
+      (occ,t)
+  and substrec except k occ c t =
+    if eq_constr t c then
+      if except then 
+	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
+      else 
+	if List.mem occ locs then (occ+1,Rel(k)) else  (occ+1,t)
+    else 
+      match t with
+	| DOPN(Const sp,tl) -> occ,t
+	|  DOPN(MutConstruct _,tl) -> occ,t
+	|  DOPN(MutInd _,tl) -> occ,t
+	|  DOPN(i,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = substcheck except k nocc' c f in
+                    (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DOPN(i,Array.of_list (List.rev cl')))
+	|  DOP2(i,t1,t2) -> 
+	     let (nocc1,t1')=substrec except k occ c t1 in
+             let (nocc2,t2')=substcheck except k nocc1 c t2 in
+             nocc2,DOP2(i,t1',t2')
+	|  DOP1(i,t) -> 
+	     let (nocc,t')= substrec except k occ c t in
+	     nocc,DOP1(i,t')
+	|  DLAM(n,t) -> 
+	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
+             (occ',DLAM(n,t'))
+	|  DLAMV(n,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = 
+		      substcheck except (k+1) nocc' (lift 1 c) f
+                    in (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
+	|  _ -> occ,t
+  in 
+  if locs = [] then 
+    subst_term c t
+  else if List.mem 0 locs then 
+    t
+  else 
+    let except = List.for_all (fun n -> n<0) locs in
+    let (nbocc,t') = substcheck except 1 1 c t in
+    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
+      failwith "subst_term_occ: too few occurences";
+    t'
+
   
 (***************************)
 (* occurs check functions  *)                         
@@ -1154,6 +1219,18 @@ let rec occur_meta = function
 
 let rel_vect = (Generic.rel_vect : int -> int -> constr array)
 		 
+let occur_existential = 
+  let rec occrec = function
+    | DOPN(Evar _,_) -> true
+    | DOPN(_,cl) -> array_exists occrec cl
+    | DOPL(_,cl) -> List.exists occrec cl
+    | DOP2(_,c1,c2) -> occrec c1 or occrec c2
+    | DOP1(_,c) -> occrec c
+    | DLAM(_,c) -> occrec c
+    | DLAMV(_,cl) -> array_exists occrec cl
+    | _ -> false
+  in 
+  occrec
 
 (***************************)
 (* hash-consing functions  *)                         
diff --git a/kernel/term.mli b/kernel/term.mli
index 823917ea5f..5118d39c5d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -474,6 +474,7 @@ val sort_hdchar : sorts -> string
 (*s Occur check functions. *)                         
 
 val occur_meta : constr -> bool
+val occur_existential : constr -> bool
 val rel_vect : int -> int -> constr array
 
 (* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs 
@@ -492,6 +493,7 @@ val subst_term : constr -> constr -> constr
 val subst_term_eta_eq : constr -> constr -> constr
 val replace_consts :
   (section_path * (identifier list * constr) option) list -> constr -> constr
+val subst_term_occ : int list -> constr -> constr -> constr
 
 (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
    for each binding $(i,c_i)$ in [bl],
diff --git a/lib/util.ml b/lib/util.ml
index 7f726fe0ed..d165c157b2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -51,6 +51,10 @@ let parse_section_path s =
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
+let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
+
+let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
@@ -189,7 +193,12 @@ let list_prefix_of prefl l =
     | (_, _) -> false
   in 
   prefrec (prefl,l)
-    
+
+let list_map_append f l = List.flatten (List.map f l)
+
+let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
+
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index 77c87c5288..bcdf4493c6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -28,6 +28,9 @@ val parse_section_path : string -> string list * string * string
 
 module Stringmap : Map.S with type key = string
 
+val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
+val stringmap_dom : 'a Stringmap.t -> string list
+
 (*s Lists. *)
 
 val list_intersect : 'a list -> 'a list -> 'a list
@@ -54,6 +57,10 @@ 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
+(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
+(* raises [Invalid_argument] if the two lists don't have the same length *)
+val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 
 (*s Arrays. *)
 
@@ -72,7 +79,7 @@ val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
 val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_app_tl : 'a array -> 'a list -> 'a list
 val array_list_of_tl : 'a array -> 'a list
-val array_map_to_list : ('a -> 'b) -> 'a array ->'b 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 : 
diff --git a/library/declare.ml b/library/declare.ml
index 00f1fbf8d8..6336c03c6f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -8,9 +8,11 @@ open Term
 open Sign
 open Constant
 open Inductive
+open Reduction
 open Libobject
 open Lib
 open Impargs
+open Indrec
 
 type strength = 
   | DischargeAt of section_path 
@@ -132,7 +134,6 @@ let declare_mind mie =
   Global.add_mind sp mie;
   push_inductive_names sp mie;
   declare_inductive_implicits sp
-  (***TODO: declare_eliminations ***)
 
 (* Global references. *)
 
@@ -169,7 +170,7 @@ let global_reference kind id =
   let sp = Nametab.sp_of_id kind id in
   let oper = global_operator sp id in
   let hyps = get_globals (Global.context ()) in
-  let ids =  ids_of_sign hyps in
+  let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
 let is_global id =
@@ -192,3 +193,30 @@ let mind_path = function
       let (pa,_,k) = repr_path sp in 
       Names.make_path pa (mip.mind_consnames.(ind-1)) k 
   | _ -> invalid_arg "mind_path"
+
+(* Eliminations. *)
+
+let declare_eliminations sp =
+  let env = Global.unsafe_env () in
+  let sigma = Evd.empty in
+  let mindid = basename sp in
+  let mind = global_reference (kind_of_path sp) mindid in
+  let redmind = minductype_spec env sigma mind in
+  let mindstr = string_of_id mindid in
+  let declare na c =
+    declare_constant (id_of_string na) 
+      { const_entry_body = c; const_entry_type = None } in
+  let mispec = Global.lookup_mind_specif redmind in 
+  let elim_scheme = 
+    strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in
+  let npars = mis_nparams mispec in
+  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
+  let kelim = mis_kelim mispec in
+  if List.mem prop kelim then
+    declare (mindstr^"_ind") (make_elim prop);
+  if List.mem spec kelim then
+    declare (mindstr^"_rec") (make_elim spec);
+  if List.mem types kelim then
+    declare (mindstr^"_rect") (make_elim (Type (Univ.new_univ sp)))
+
+      
diff --git a/library/declare.mli b/library/declare.mli
index c2944c330a..e833d0bb80 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -12,8 +12,8 @@ open Inductive
    parameters, constants and inductive types. Using the following functions
    will add the entries in the global environment (module [Global]), will
    register the declarations in the library (module [Lib]) --- so that the
-   reset works properly --- and will fill some global tables as [Nametab] and
-   [Impargs]. *)
+   reset works properly --- and will fill some global tables such as 
+   [Nametab] and [Impargs]. *)
 
 type strength = 
   | DischargeAt of section_path 
@@ -27,6 +27,8 @@ val declare_constant : identifier -> constant_entry -> unit
 
 val declare_mind : mutual_inductive_entry -> unit
 
+val declare_eliminations : section_path -> unit
+
 
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 21fc10bf73..4c14040bdd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -426,9 +426,8 @@ let clenv_val_of clenv mv =
       (match Intmap.find mv clenv.env with
 	 | Cltyp _ -> DOP0(Meta mv)
 	 | Clval(b,_) ->
-	     instance (List.map (fun mv' -> (mv',valrec mv')) 
-			 (Intset.elements b.freemetas)) 
-	       (w_env clenv.hook) (w_Underlying clenv.hook) b.rebus)
+	     plain_instance (List.map (fun mv' -> (mv',valrec mv')) 
+			       (Intset.elements b.freemetas)) b.rebus)
     with Not_found -> 
       DOP0(Meta mv)
   in 
@@ -439,7 +438,7 @@ let clenv_instance clenv b =
     List.map 
       (fun mv -> (mv,clenv_val_of clenv mv)) (Intset.elements b.freemetas)
   in 
-  instance c_sigma (w_env clenv.hook) (w_Underlying clenv.hook) b.rebus
+  plain_instance c_sigma b.rebus
     
 let clenv_instance_term clenv c =
   clenv_instance clenv (mk_freelisted c)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index de56125af5..f5daf8b361 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -69,7 +69,7 @@ val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
 val clenv_independent : 
   wc clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_missing : 
-  wc clausenv -> constr freelisted * constr freelisted -> int list
+  'a clausenv -> constr freelisted * constr freelisted -> int list
 val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 val clenv_lookup_name : 'a clausenv -> identifier -> int
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
index 59069fc046..ccaaae4fb3 100644
--- a/proofs/tacred.mli
+++ b/proofs/tacred.mli
@@ -9,7 +9,7 @@ open Evd
 open Reduction
 (*i*)
 
-(* Reduction functions associated to tactics. *)
+(* Reduction functions associated to tactics. \label{tacred} *)
 
 val hnf_constr : 'a reduction_function
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
new file mode 100644
index 0000000000..634e71f99a
--- /dev/null
+++ b/tactics/auto.ml
@@ -0,0 +1,922 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Inductive
+open Evd
+open Reduction
+open Typing_ev
+open Tacmach
+open Proof_trees
+open Pfedit
+open Tacred
+open Tactics
+open Tacticals
+open Clenv
+open Hiddentac
+open Libobject
+open Library
+open Vernacinterp
+
+(****************************************************************************)
+(*            The Type of Constructions Autotactic Hints                    *)
+(****************************************************************************)
+
+type auto_tactic = 
+  | Res_pf     of constr * unit clausenv (* Hint Apply *)
+  | ERes_pf    of constr * unit clausenv (* Hint EApply *)
+  | Give_exact of constr                  
+  | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+  | Unfold_nth of constr                 (* Hint Unfold *)
+  | Extern of CoqAst.t                   (* Hint Extern *) 
+
+type pri_auto_tactic = { 
+  hname : identifier;    (* name of the hint *)
+  pri  : int;            (* A number between 0 and 4, 4 = lower priority *)
+  pat  : constr option;  (* A pattern for the concl of the Goal *)
+  code : auto_tactic     (* the tactic to apply when the concl matches pat *)
+}
+
+let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2
+
+let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2
+
+let insert v l = 
+  let rec insrec = function
+    | [] -> [v]
+    | h::tl -> if pri_order v h then v::h::tl else h::(insrec tl)
+  in 
+  insrec l
+
+(* Nov 98 -- Papageno *)
+(* Les Hints sont ré-organisés en plusieurs databases. 
+
+  La table impérative "searchtable", de type "hint_db_table",
+   associe une database (hint_db) à chaque nom.
+
+  Une hint_db est une table d'association fonctionelle constr -> search_entry
+  Le constr correspond à la constante de tête de la conclusion.
+
+  Une search_entry est un triplet comprenant :
+     - la liste des tactiques qui n'ont pas de pattern associé
+     - la liste des tactiques qui ont un pattern
+     - un discrimination net borné (Btermdn.t) constitué de tous les
+       patterns de la seconde liste de tactiques *)
+
+type stored_data = pri_auto_tactic
+
+type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
+
+let empty_se = ([],[],Btermdn.create ())
+
+let add_tac t (l,l',dn) =
+  match t.pat with
+      None -> (insert t l, l', dn)
+    | Some pat -> (l, insert t l', Btermdn.add dn (pat,t))
+
+
+let lookup_tacs (hdc,c) (l,l',dn) =
+  let l'  = List.map snd (Btermdn.lookup dn c) in
+  let sl' = Sort.list pri_order l' in
+    Sort.merge pri_order l sl'
+
+
+module Constr_map = Map.Make(struct 
+			       type t = constr 
+			       let compare = Pervasives.compare 
+			     end)
+
+module Hint_db = struct
+
+  type t = search_entry Constr_map.t
+
+  let empty = Constr_map.empty
+
+  let find key db =
+    try Constr_map.find key db
+    with Not_found -> empty_se
+
+  let map_all k db =
+    let (l,l',_) = find k db in
+      Sort.merge pri_order l l'
+   
+  let map_auto (k,c) db =
+    lookup_tacs (k,c) (find k db)
+
+  let add_one (k,v) db =
+    let oval = find k db in 
+      Constr_map.add k (add_tac v oval) db
+
+  let add_list l db = List.fold_right add_one l db
+
+  let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db
+
+end
+
+type frozen_hint_db_table = Hint_db.t Stringmap.t 
+
+type hint_db_table = Hint_db.t Stringmap.t
+
+let searchtable  = ref (Stringmap.empty : hint_db_table)
+
+let searchtable_map name = 
+  Stringmap.find name !searchtable
+let searchtable_add (name,db) = 
+  searchtable := Stringmap.add name db !searchtable
+
+(**************************************************************************)
+(*                       Definition of the summary                        *)
+(**************************************************************************)
+
+let init     () = searchtable := Stringmap.empty
+let freeze   () = !searchtable
+let unfreeze fs = searchtable := fs
+
+let _ = Summary.declare_summary "search"
+	  { Summary.freeze_function   = freeze;
+	    Summary.unfreeze_function = unfreeze;
+	    Summary.init_function     = init }
+
+ 
+(**************************************************************************)
+(*               declaration of the AUTOHINT library object               *)
+(**************************************************************************)
+
+(* If the database does not exist, it is created *)
+(* TODO: should a warning be printed in this case ?? *)
+let add_hint dbname hintlist = 
+  try 
+    let db = searchtable_map dbname in
+    let db' = Hint_db.add_list hintlist db in
+    searchtable_add (dbname,db')
+  with Not_found -> 
+    let db = Hint_db.add_list hintlist Hint_db.empty in
+    searchtable_add (dbname,db)
+
+let cache_autohint (_,(name,hintlist)) =
+  try add_hint name hintlist with _ -> anomaly "Auto.add_hint"
+
+let specification_autohint x = x
+
+let (inAutoHint,outAutoHint) =
+  declare_object ("AUTOHINT",
+                  { load_function = (fun _ -> ());
+                    cache_function = cache_autohint;
+		    open_function = (fun _ -> ());
+                    specification_function = specification_autohint })
+
+(**************************************************************************)
+(*                     The "Hint" vernacular command                      *)
+(**************************************************************************)
+
+let rec nb_hyp = function
+  | DOP2(Prod,_,DLAM(_,c2)) -> 
+      if dependent (Rel 1) c2 then nb_hyp c2 else 1+(nb_hyp c2)
+  | _ -> 0 
+
+(* adding and removing tactics in the search table *)
+
+let make_exact_entry name (c,cty) =
+  match strip_outer_cast cty with
+    | DOP2(Prod,_,_) -> 
+	failwith "make_exact_entry"
+    | cty -> 
+	(List.hd (head_constr cty),
+	 { hname=name; pri=0; pat=None; code=Give_exact c })
+
+let make_apply_entry (eapply,verbose) name (c,cty) =
+  match hnf_constr (Global.unsafe_env()) Evd.empty cty with
+    | DOP2(Prod,_,_) as cty ->
+        let hdconstr = (try  List.hd (head_constr_bound cty [])  
+                        with Bound -> failwith "make_apply_entry") in
+        let ce = mk_clenv_from () (c,cty) in 
+        let nmiss = 
+	  List.length 
+            (clenv_missing ce (clenv_template ce,clenv_template_type ce)) 
+        in 
+	if eapply & (nmiss <> 0) then begin
+          if verbose then 
+	    wARN [< 'sTR "the hint: EApply "; prterm c;
+		    'sTR " will only used by EAuto" >]; 
+          (hdconstr,
+           { hname = name;
+	     pri = nb_hyp cty + nmiss;
+             pat = Some (clenv_template_type ce).rebus;
+             code = ERes_pf(c,ce) })
+        end else 
+	  (hdconstr,
+           { hname = name;
+	     pri = nb_hyp cty;
+             pat = Some (clenv_template_type ce).rebus;
+             code = Res_pf(c,ce) })
+    | _ -> failwith "make_apply_entry"
+ 
+(* eap is (e,v) with e=true if eapply and v=true if verbose 
+   c is a constr
+   cty is the type of constr *)
+
+let make_resolves name eap (c,cty) =
+  let ents = 
+    map_succeed 
+      (fun f -> f name (c,cty)) 
+      [make_exact_entry; make_apply_entry eap]
+  in 
+  if ents = [] then 
+    errorlabstrm "Hint" [< pTERM c; 'sPC; 'sTR "cannot be used as a hint" >];
+  ents
+
+(* used to add an hypothesis to the local hint database *)
+let make_resolve_hyp hname htyp = 
+  try
+    [make_apply_entry (true, false) hname (mkVar hname, htyp)]
+  with 
+    | Failure _ -> []
+    | UserError _ -> anomaly "Papageno programme comme un blaireau"
+
+let add_resolves clist dbnames =
+  List.iter 
+    (fun dbname ->
+       Lib.add_anonymous_leaf
+	 (inAutoHint
+	    (dbname,
+     	     (List.flatten
+		(List.map (fun (name,c) -> 
+			     let env = Global.unsafe_env() in
+			     let ty = type_of env Evd.empty c in
+			     make_resolves name (true,true) (c,ty)) clist))
+	    )))
+    dbnames
+
+(* REM : in most cases hintname = id *)
+
+let make_unfold (hintname, id) =
+  let hdconstr = 
+    (try 
+       Declare.global_reference CCI id
+     with Not_found -> 
+       errorlabstrm  "make_unfold" [<print_id id; 'sTR " not declared" >])
+  in 
+  (hdconstr, 
+   { hname = hintname;
+     pri = 4;
+     pat = None;
+     code = Unfold_nth hdconstr })
+
+let add_unfolds l dbnames =
+  List.iter 
+    (fun dbname ->
+       Lib.add_anonymous_leaf (inAutoHint (dbname, List.map make_unfold l)))
+    dbnames
+
+let make_extern name pri pat tacast = 
+  let hdconstr = List.hd (head_constr pat) in 
+  (hdconstr,
+   { hname = name;
+     pri=pri;
+     pat = Some pat;
+     code= Extern tacast })
+
+let add_extern name pri pat tacast dbname =
+  (* We check that all metas that appear in tacast have at least
+     one occurence in the left pattern pat *)
+  let tacmetas = CoqAst.collect_metas tacast in 
+  let patmetas = Clenv.collect_metas pat in
+  match (subtract tacmetas patmetas) with
+    | i::_ ->
+	errorlabstrm "add_extern" 
+	  [< 'sTR "The meta-variable ?"; 'iNT i; 'sTR" is not bound" >]
+    | []  ->
+	add_anonymous_object 
+	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
+
+let add_externs name pri pat tacast dbnames = 
+  List.iter (add_extern name pri pat tacast) dbnames
+
+let make_trivial (name,c) =
+  let sigma = Evd.empty and env = Global.unsafe_env() in
+  let t = type_of env sigma c in
+  let hdconstr = List.hd (head_constr t) in
+  let ce = mk_clenv_from () (c,hnf_constr env sigma t) in
+  (hdconstr, { hname = name;
+	       pri=1;
+               pat = Some(clenv_template_type ce).rebus;
+               code=Res_pf_THEN_trivial_fail(c,ce) })
+
+let add_trivials l dbnames =
+  List.iter
+    (fun dbname ->
+       Lib.add_anonymous_leaf (inAutoHint(dbname, List.map make_trivial l)))
+    dbnames
+
+let _ = 
+  vinterp_add
+    "HintUnfold"
+    (function 
+       | [ VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_IDENTIFIER id] ->
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function VARG_IDENTIFIER i -> string_of_id i
+		      	 | _ -> bad_vernac_args "HintUnfold") l in
+      	   fun () -> add_unfolds [(hintname, id)] dbnames
+       | _-> bad_vernac_args "HintUnfold")
+    
+let _ = 
+  vinterp_add
+    "HintResolve"
+    (function 
+       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
+	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function VARG_IDENTIFIER i -> string_of_id i
+		      	 | _ -> bad_vernac_args "HintResolve") l in
+	   fun () -> add_resolves [hintname, c1] dbnames
+       | _-> bad_vernac_args "HintResolve" )
+   
+let _ = 
+  vinterp_add
+    "HintImmediate"
+    (function 
+       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
+	   let c1 = Trad.constr_of_com (Evd.mt_evd()) (initial_sign()) c in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function VARG_IDENTIFIER i -> string_of_id i
+			 | _ -> bad_vernac_args "HintImmediate") l in
+	   fun () -> add_trivials [hintname, c1] dbnames
+       | _ -> bad_vernac_args "HintImmediate")
+
+let _ = 
+  vinterp_add
+    "HintConstructors"
+    (function 
+       | [VARG_IDENTIFIER idr; VARG_VARGLIST l; VARG_IDENTIFIER c] ->
+	   begin 
+	     try
+	       let trad = Declare.global_reference CCI in
+	       let rectype = trad c in
+	       let consnames = 
+		 mis_consnames (Global.lookup_mind_specif rectype) in
+	       let lcons = 
+		 array_map_to_list (fun id -> (id, trad id)) consnames in
+	       let dbnames = if l = [] then ["core"] else 
+	      	 List.map (function VARG_IDENTIFIER i -> string_of_id i
+			     | _ -> bad_vernac_args "HintConstructors") l in
+    	       fun () -> add_resolves lcons dbnames
+	     with Invalid_argument("mind_specif_of_mind") -> 
+	       error ((string_of_id c) ^ " is not an inductive type")
+	   end 
+       | _ -> bad_vernac_args "HintConstructors")
+    
+let _ = 
+  vinterp_add
+    "HintExtern"
+    (function 
+       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
+	  VARG_NUMBER pri; VARG_COMMAND patcom; VARG_TACTIC tacexp] ->
+           let pat = Pattern.raw_sopattern_of_compattern 
+		       (initial_sign()) patcom in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function VARG_IDENTIFIER i -> string_of_id i
+		      	 | _ -> bad_vernac_args "HintConstructors") l in
+           fun () -> add_externs hintname pri pat tacexp dbnames
+       | _ -> bad_vernac_args "HintExtern")
+
+let _ = 
+  vinterp_add
+    "HintsResolve"
+    (function
+       | (VARG_VARGLIST l)::lh ->
+ 	   let lhints = 
+	     List.map (function
+			 | VARG_IDENTIFIER i -> 
+			     (i, Declare.global_reference CCI i)
+		      	 | _-> bad_vernac_args "HintsResolve") lh in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function VARG_IDENTIFIER i -> string_of_id i
+		      	 | _-> bad_vernac_args "HintsResolve") l in
+	   fun () -> add_resolves lhints dbnames
+       | _-> bad_vernac_args "HintsResolve")
+    
+let _ = 
+  vinterp_add
+    "HintsUnfold"
+    (function
+       | (VARG_VARGLIST l)::lh ->
+	   let lhints = 
+	     List.map (function
+			 | VARG_IDENTIFIER i -> (i, i)
+		      	 | _ -> bad_vernac_args "HintsUnfold") lh in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function 
+			 | VARG_IDENTIFIER i -> string_of_id i
+		      	 | _ -> bad_vernac_args "HintsUnfold") l in
+	   fun () -> add_unfolds lhints dbnames
+       | _ -> bad_vernac_args "HintsUnfold")
+    
+let _ = 
+  vinterp_add
+    "HintsImmediate"
+    (function
+       | (VARG_VARGLIST l)::lh ->
+	   let lhints = 
+	     List.map (function
+			 | VARG_IDENTIFIER i -> 
+			     (i, Declare.global_reference CCI i)
+		      	 | _ -> bad_vernac_args "HintsImmediate") lh in
+	   let dbnames = if l = [] then ["core"] else 
+	     List.map (function 
+			 | VARG_IDENTIFIER i -> string_of_id i
+		      	 | _ -> bad_vernac_args "HintsImmediate") l in
+	   fun () -> add_trivials lhints dbnames
+       | _-> bad_vernac_args "HintsImmediate")
+    
+(**************************************************************************)
+(*                    Functions for printing the hints                    *)
+(**************************************************************************)
+
+let fmt_autotactic = function
+  | Res_pf (c,clenv) -> [< 'sTR"Apply "; prterm c >]
+  | ERes_pf (c,clenv) -> [< 'sTR"EApply "; prterm c >]
+  | Give_exact c -> [< 'sTR"Exact " ; prterm c >]
+  | Res_pf_THEN_trivial_fail (c,clenv) -> 
+      [< 'sTR"Apply "; prterm c ; 'sTR" ; Trivial" >]
+  | Unfold_nth c -> [< 'sTR"Unfold " ;  prterm c >]
+  | Extern coqast -> [< 'sTR "Extern "; gentacpr coqast >]
+
+let fmt_hint_list hintlist =
+  [< prlist 
+       (function v ->
+          [< fmt_autotactic v.code ; 'sTR"(" ; 'iNT v.pri;
+	     'sTR")"; 'sPC >]) 
+       hintlist >]
+
+(* Print all hints associated to head c in any database *)
+let fmt_hint_list_for_head c = 
+  let dbs = stringmap_to_list !searchtable in
+  let valid_dbs = 
+    map_succeed 
+      (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
+      dbs 
+  in
+  if valid_dbs = [] then 
+    [<'sTR "No hint declared for :"; prterm c >]
+  else 
+    hOV 0 
+      [< 'sTR"For "; prterm c; 'sTR" -> ";
+	 prlist (fun (name,db,hintlist) ->
+	 	   [< 'sTR "  In the database "; 'sTR name; 'sTR " :"; 'fNL;
+		      fmt_hint_list hintlist >])
+	   valid_dbs >]
+
+let fmt_hint_id id = 
+  try 
+    let c = Declare.global_reference CCI id in fmt_hint_list_for_head c
+  with Not_found -> 
+    [< print_id id; 'sTR " not declared" >]
+
+(* Print all hints associated to head id in any database *)
+let print_hint_id id =  pPNL(fmt_hint_id id)
+
+let fmt_hint_term cl = 
+  try 
+    let (hdc,args) = match head_constr_bound cl [] with 
+      | hdc::args -> (hdc,args)
+      | [] -> assert false 
+    in
+    let dbs = stringmap_to_list !searchtable in
+    let valid_dbs = 
+      if occur_existential cl then 
+	map_succeed 
+	  (fun (name, db) -> (name, db, Hint_db.map_all hdc db)) 
+	  dbs
+      else 
+	map_succeed 
+	  (fun (name, db) -> 
+	     (name, db, Hint_db.map_auto (hdc,applist(hdc,args)) db)) 
+	  dbs
+    in 
+    if valid_dbs = [] then 
+      [<'sTR "No hint applicable for current goal" >]
+    else 
+      [< 'sTR "Applicable Hints :";
+	 prlist (fun (name,db,hintlist) ->
+	 	   [< 'sTR "  In the database "; 'sTR name; 
+		      'sTR " :"; 'fNL;
+		      fmt_hint_list hintlist >])
+	   valid_dbs >]
+  with BOUND | Match_failure _ | Failure _ -> 
+    [<'sTR "No hint applicable for current goal" >]
+	  
+let print_hint_term cl = pPNL (fmt_hint_term cl)
+
+(* print all hints that apply to the concl of the current goal *)
+let print_applicable_hint () = 
+  let pts = get_pftreestate () in 
+  let gl = nth_goal_of_pftreestate 1 pts in 
+  print_hint_term (pf_concl gl)
+    
+(* displays the whole hint database db *)
+let print_hint_db db =
+  Hint_db.iter 
+    (fun head hintlist ->
+       mSG (hOV 0 
+	      [< 'sTR "For "; prterm head; 'sTR " -> "; 
+		 fmt_hint_list hintlist; 'fNL >]))
+    db
+
+let print_hint_db_by_name dbname =
+  try 
+    let db = searchtable_map dbname in print_hint_db db
+  with Not_found -> 
+    error (dbname^" : No such Hint database")
+  
+(* displays all the hints of all databases *)
+let print_searchtable () =
+  Stringmap.iter
+    (fun name db ->
+       mSG [< 'sTR "In the database "; 'sTR name; 'fNL >];
+       print_hint_db db)
+    !searchtable
+
+let _ = 
+  vinterp_add("PrintHint",
+	      function 
+		| [] -> fun () -> print_searchtable()
+	        | _ -> assert false)
+
+let _ = 
+  vinterp_add("PrintHintDb",
+	      function 
+	      	| [(VARG_IDENTIFIER id)] -> 
+		    fun () -> print_hint_db_by_name (string_of_id id)
+	      	| _ -> assert false)
+
+let _ = 
+  vinterp_add("PrintHintGoal",
+	      function 
+		| [] -> fun () -> print_applicable_hint()
+	        | _ -> assert false)
+    
+let _ = 
+  vinterp_add("PrintHintId",
+	      function 
+		| [(VARG_IDENTIFIER id)] -> fun () -> print_hint_id id
+	        | _ -> assert false)
+
+(**************************************************************************)
+(*                           Automatic tactics                            *)
+(**************************************************************************)
+
+(**************************************************************************)
+(*          tactics with a trace mechanism for automatic search           *)
+(**************************************************************************)
+
+let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
+
+
+(* Try unification with the precompiled clause, then use registered Apply *)
+
+let unify_resolve (c,clenv) gls = 
+  let (wc,kONT) = startWalk gls in
+  let clenv' = connect_clenv wc clenv in
+  let _ = clenv_unique_resolver false clenv' gls in  
+  h_simplest_apply c gls
+
+(* builds a hint database from a constr signature *)
+(* typically used with (lid, ltyp) = pf_untyped_hyps <some goal> *)
+
+let make_local_hint_db (lid, ltyp) = 
+  let hintlist = list_map_append2 make_resolve_hyp lid ltyp in
+  Hint_db.add_list hintlist Hint_db.empty
+
+
+(**************************************************************************)
+(*                           The Trivial tactic                           *)
+(**************************************************************************)
+
+(* local_db is a Hint database containing the hypotheses of current goal *)
+(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+
+let rec trivial_fail_db db_list local_db gl =
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g'->
+	 let (hn, htyp) = hd_sign (pf_untyped_hyps g') in
+	 let hintl = make_resolve_hyp hn htyp in
+	 trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
+  in
+  tclFIRST 
+    (assumption::intro_tac::
+     (List.map tclCOMPLETE 
+	(trivial_resolve db_list local_db (pf_concl gl)))) gl
+
+and my_find_search db_list local_db hdc concl =
+  let tacl = 
+    if occur_existential concl then 
+      list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list)
+    else 
+      list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db)
+      	(local_db::db_list)
+  in
+  List.map 
+    (fun ({pri=b; pat=p; code=t} as patac) -> 
+       (b,
+	match t with
+	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
+	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
+	  | Give_exact c  -> exact c
+	  | Res_pf_THEN_trivial_fail (term,cl) -> 
+	      tclTHEN 
+		(unify_resolve (term,cl)) 
+		(trivial_fail_db db_list local_db)
+	  | Unfold_nth c -> unfold_constr c
+	  | Extern tacast -> 
+	      conclPattern concl (outSOME p) tacast))
+    tacl
+
+and trivial_resolve db_list local_db cl = 
+  try 
+    priority 
+      (my_find_search db_list local_db (List.hd (head_constr_bound cl [])) cl)
+  with Bound | Not_found -> 
+    []
+
+let trivial dbnames gl =
+  let db_list = 
+    List.map
+      (fun x -> 
+	 try 
+	   searchtable_map x
+	 with Not_found -> 
+	   error ("Trivial: "^x^": No such Hint database"))
+      ("core"::dbnames) 
+  in
+  tclTRY 
+    (trivial_fail_db db_list (make_local_hint_db (pf_untyped_hyps gl))) gl 
+    
+let full_trivial gl =
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames = list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_untyped_hyps gl))) gl
+
+let dyn_trivial = function
+  | []                  -> trivial []
+  | [Quoted_string "*"] -> full_trivial
+  | l -> trivial (List.map 
+		    (function 
+		       | Identifier id -> (string_of_id id)
+		       | other -> bad_tactic_args "dyn_trivial" [other]) 
+		    l)
+   
+let h_trivial = hide_tactic "Trivial" dyn_trivial
+
+(**************************************************************************)
+(*                       The classical Auto tactic                        *)
+(**************************************************************************)
+
+let possible_resolve db_list local_db cl =
+  try 
+    List.map snd 
+      (my_find_search db_list local_db 
+	 (List.hd (head_constr_bound cl [])) cl)
+  with Bound | Not_found -> 
+    []
+
+let decomp_unary_term c gls = 
+  let typc = pf_type_of gls c in 
+  let hd = List.hd (head_constr typc) in 
+  if Pattern.is_conjunction hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_unary_term" [<'sTR "not a unary type" >] 
+
+let decomp_empty_term c gls = 
+  let typc = pf_type_of gls c in 
+  let (hd,_) = decomp_app typc in 
+  if Pattern.is_empty_type hd then 
+    simplest_case c gls 
+  else 
+    errorlabstrm "Auto.decomp_empty_term" [<'sTR "not an empty type" >] 
+
+
+(* decomp is an natural number giving an indication on decomposition 
+   of conjunction in hypotheses, 0 corresponds to no decomposition *)
+(* n is the max depth of search *)
+(* local_db contains the local Hypotheses *)
+
+let rec search_gen decomp n db_list local_db add_sign goal =
+  if n=0 then error "BOUND 2";
+  let decomp_tacs = match decomp with 
+    | 0 -> [] 
+    | p -> 
+	(tclTRY_sign decomp_empty_term add_sign)
+	::
+	(List.map 
+	   (fun id -> tclTHEN (decomp_unary_term (VAR id)) 
+		(tclTHEN 
+		   (clear_one id)
+		   (search_gen decomp p db_list local_db nil_sign)))
+	   (fst (pf_untyped_hyps goal))) 
+  in
+  let intro_tac = 
+    tclTHEN intro 
+      (fun g' -> 
+	 let (hid,htyp) = hd_sign (pf_untyped_hyps g') in
+	 let hintl = 
+	   try 
+	     [make_apply_entry (true,false) hid (mkVar hid,htyp)]
+	   with Failure _ -> [] 
+	 in
+         search_gen decomp n db_list
+	   (Hint_db.add_list hintl local_db) ([hid],[htyp]) g') 
+  in
+  let rec_tacs = 
+    List.map 
+      (fun ntac -> 
+	 tclTHEN ntac 
+	   (search_gen decomp (n-1) db_list local_db nil_sign))
+      (possible_resolve db_list local_db (pf_concl goal))
+  in 
+  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
+
+
+let search = search_gen 0
+
+let default_search_depth = ref 5
+			     
+let auto n dbnames gl = 
+  let db_list = 
+    List.map
+      (fun x -> 
+	 try 
+	   searchtable_map x
+	 with Not_found -> 
+	   error ("Auto: "^x^": No such Hint database"))
+      ("core"::dbnames) 
+  in
+  let hyps = (pf_untyped_hyps gl) in
+  tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
+
+let default_auto = auto !default_search_depth []
+
+let full_auto n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames = list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let hyps = (pf_untyped_hyps gl) in
+  tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
+  
+let default_full_auto gl = full_auto !default_search_depth gl
+
+let dyn_auto l = match l with
+  | []          -> auto !default_search_depth []
+  | [Integer n] -> auto n []
+  | [Quoted_string "*"] -> default_full_auto 
+  | [Integer n; Quoted_string "*"] -> full_auto n
+  | (Integer n)::l1 -> 
+      auto n (List.map 
+		(function 
+		   | Identifier id -> (string_of_id id)
+		   | other -> bad_tactic_args "dyn_auto" [other]) l1)
+  | _ -> 
+      auto !default_search_depth 
+	(List.map 
+	   (function 
+	      | Identifier id -> (string_of_id id)
+	      | other -> bad_tactic_args "dyn_auto" [other]) l)
+
+let h_auto = hide_tactic "Auto" dyn_auto 
+
+(**************************************************************************)
+(*                  The "destructing Auto" from Eduardo                   *)
+(**************************************************************************)
+
+(* Depth of search after decomposition of hypothesis, by default 
+   one look for an immediate solution *) 
+(* Papageno : de toute façon un paramète > 1 est traité comme 1 pour 
+   l'instant *)
+let default_search_decomp = ref 1
+
+let destruct_auto des_opt n gl = 
+  let hyps = pf_untyped_hyps gl in
+  search_gen des_opt n [searchtable_map "core"] 
+    (make_local_hint_db hyps) hyps gl
+    
+let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
+
+let default_dauto = dautomatic !default_search_decomp !default_search_depth
+
+let dyn_dauto = function
+  | []          -> default_dauto
+  | [Integer n] -> dautomatic !default_search_decomp n
+  | [Integer n; Integer p] -> dautomatic p n
+  | _           -> invalid_arg "DAuto: non numeric arguments"
+     
+let dauto =
+  let gentac = hide_tactic "DAuto" dyn_dauto in
+  function
+    | (None, None)     -> gentac []
+    | (Some n, None)   -> gentac [Integer n]
+    | (Some n, Some p) -> gentac [Integer n; Integer p]
+    | _ -> assert false
+
+(***************************************)
+(*** A new formulation of Auto *********)
+(***************************************)
+
+type autoArguments =
+  | UsingTDB       
+  | Destructing   
+
+let keepAfter tac1 tac2 = 
+  (tclTHEN tac1 
+     (function g -> tac2 (make_sign [hd_sign (pf_untyped_hyps g)]) g))
+
+let compileAutoArg contac = function
+  | Destructing -> 
+      (function g -> 
+         let ctx =(pf_untyped_hyps g) in  
+	 tclFIRST 
+           (List.map2 
+              (fun id typ -> 
+                 if (Pattern.is_conjunction (hd_of_prod typ)) then 
+		   (tclTHEN
+                      (tclTHEN (simplest_elim (mkVar id)) 
+                         (clear_one id))
+                      contac) 
+                 else 
+		   tclFAIL)
+	      (fst ctx) (snd ctx)) g)
+  | UsingTDB ->  
+      (tclTHEN  
+         (Tacticals.tryAllClauses 
+            (function 
+               | Some id -> Dhyp.dHyp id
+               | None    -> Dhyp.dConcl))
+         contac)
+
+let compileAutoArgList contac = List.map (compileAutoArg contac)
+
+let rec super_search n db_list local_db argl goal =
+  if n = 0 then error "BOUND 2";
+  tclFIRST
+    (assumption
+     ::
+     (tclTHEN intro 
+        (fun g -> 
+	   let (hid,htyp) = hd_sign (pf_untyped_hyps g) in
+	   let hintl = make_resolves hid (true,false) (mkVar hid,htyp) in
+	   super_search n db_list (Hint_db.add_list hintl local_db)
+	     argl g))
+     ::
+     ((List.map 
+         (fun ntac -> 
+            tclTHEN ntac 
+              (super_search (n-1) db_list local_db argl))
+         (possible_resolve db_list local_db (pf_concl goal)))
+      @
+      (compileAutoArgList  
+         (super_search (n-1) db_list local_db argl) argl))) goal
+
+let search_superauto n ids argl g = 
+  let sigma = 
+    ids,
+    (List.map (fun id -> pf_type_of g (pf_global g id)) ids) in   
+  let hyps = (concat_sign (pf_untyped_hyps g) sigma) in
+  super_search n [Fmavm.map searchtable "core"] (make_local_hint_db hyps)
+    argl g
+
+let superauto n ids_add argl  = 
+  tclTRY (tclCOMPLETE (search_superauto n ids_add argl))
+
+let default_superauto g = superauto !default_search_depth [] [] g
+
+let cvt_autoArgs = function
+  | "Destructing"  -> [Destructing]
+  | "UsingTDB"     -> [UsingTDB]
+  | "NoAutoArg"    -> []
+  | x -> errorlabstrm "cvt_autoArgs"
+        [< 'sTR "Unexpected argument for Auto!"; 'sTR x >]
+
+let dyn_superauto l g = 
+  match l with
+    | (Integer n)::(Clause ids_add)::l -> 
+        superauto n ids_add 
+          (join_map_list 
+             (function 
+		| Quoted_string s -> (cvt_autoArgs s)
+                | _ -> assert false) l) g
+    | _::(Clause ids_add)::l  -> 
+        superauto !default_search_depth ids_add 
+          (join_map_list 
+             (function 
+		| Quoted_string s -> (cvt_autoArgs s)
+                | _ -> assert false) l) g
+    | l -> bad_tactic_args "SuperAuto" l g
+
+let h_superauto = hide_tactic "SuperAuto" dyn_superauto
diff --git a/tactics/auto.mli b/tactics/auto.mli
new file mode 100644
index 0000000000..01a2d5f6dd
--- /dev/null
+++ b/tactics/auto.mli
@@ -0,0 +1,143 @@
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Proof_trees
+open Tacmach
+open Clenv
+(*i*)
+  
+type auto_tactic = 
+  | Res_pf     of constr * unit clausenv (* Hint Apply *)
+  | ERes_pf    of constr * unit clausenv (* Hint EApply *)
+  | Give_exact of constr                  
+  | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+  | Unfold_nth of constr                 (* Hint Unfold *)
+  (***TODO
+  | Extern     of CoqAst.t               (* Hint Extern *)
+  ***)
+
+type pri_auto_tactic = { 
+  hname : identifier;     (* name of the hint *)
+  pri   : int;            (* A number between 0 and 4, 4 = lower priority *)
+  pat   : constr option;  (* A pattern for the concl of the Goal *)
+  code  : auto_tactic;    (* the tactic to apply when the concl matches pat *)
+}
+
+type stored_data = pri_auto_tactic 
+
+type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
+
+module Hint_db :
+  sig
+    type t
+    val empty : t
+    val find : constr -> t -> search_entry
+    val map_all : constr -> t -> pri_auto_tactic list
+    val map_auto : constr * constr -> t -> pri_auto_tactic list
+    val add_one : constr * pri_auto_tactic -> t -> t
+    val add_list : (constr * pri_auto_tactic) list -> t -> t
+    val iter : (constr -> stored_data list -> unit) -> t -> unit
+  end
+
+type frozen_hint_db_table = Hint_db.t Stringmap.t
+
+type hint_db_table = Hint_db.t Stringmap.t
+
+val searchtable : hint_db_table
+
+(* [make_exact_entry hint_name (c, ctyp)]. 
+   [hint_name] is the name of then hint;
+   [c] is the term given as an exact proof to solve the goal;
+   [ctyp] is the type of [hc]. *)
+
+val make_exact_entry :
+  identifier -> constr * constr -> constr * pri_auto_tactic
+
+(* [make_apply_entry (eapply,verbose) name (c,cty)].
+   [eapply] is true if this hint will be used only with EApply;
+   [name] is the name of then hint;
+   [c] is the term given as an exact proof to solve the goal;
+   [cty] is the type of [hc]. *)
+
+val make_apply_entry :
+  bool * bool -> identifier -> constr * constr -> constr * pri_auto_tactic
+
+(* A constr which is Hint'ed will be:
+   (1) used as an Exact, if it does not start with a product
+   (2) used as an Apply, if its HNF starts with a product, and
+       has no missing arguments.
+   (3) used as an EApply, if its HNF starts with a product, and
+       has missing arguments. *)
+
+val make_resolves :
+  identifier -> bool * bool -> constr * constr -> 
+    (constr * pri_auto_tactic) list
+
+(* [make_resolve_hyp hname htyp].
+   used to add an hypothesis to the local hint database;
+   Never raises an User_exception;
+   If the hyp cannot be used as a Hint, the empty list is returned. *)
+
+val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list
+
+(* [make_extern name pri pattern tactic_ast] *)
+
+(***TODO
+val make_extern :
+  identifier -> int -> constr -> CoqAst.t -> constr * pri_auto_tactic
+***)
+
+(* Create a Hint database from the pairs (name, constr).
+   Useful to take the current goal hypotheses as hints *)
+
+val make_local_hint_db : constr signature -> Hint_db.t
+
+val priority : (int * 'a) list -> 'a list
+
+val default_search_depth : int ref
+
+(* Try unification with the precompiled clause, then use registered Apply *)
+val unify_resolve : (constr * unit clausenv) -> tactic
+
+(* The Auto tactic *)
+
+val auto : int -> string list -> tactic
+
+(* auto with default search depth and with the hint database "core" *)
+val default_auto : tactic
+
+(* auto with all hint databases except the "v62" compatibility database *)
+val full_auto : int -> tactic
+
+(* auto with default search depth and with all hint databases 
+   except the "v62" compatibility database *)
+val default_full_auto : tactic
+
+(* The hidden version of auto *)
+val h_auto : tactic_arg list -> tactic
+
+(* Trivial *)
+val trivial : string list -> tactic
+val full_trivial : tactic
+val h_trivial : tactic_arg list -> tactic
+
+
+(*s The following is not yet up to date -- Papageno. *)
+
+(* DAuto *)
+val dauto : int option * int option -> tactic
+val default_search_decomp : int ref
+val default_dauto : tactic
+
+(* SuperAuto *)
+
+type autoArguments =
+  | UsingTDB       
+  | Destructing   
+
+val superauto : int -> identifier list -> autoArguments list -> tactic
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
new file mode 100644
index 0000000000..bdc0faf27c
--- /dev/null
+++ b/tactics/dhyp.ml
@@ -0,0 +1,311 @@
+
+(* $Id$ *)
+
+(* Chet's comments about this tactic :
+ 
+ Programmable destruction of hypotheses and conclusions.
+
+   The idea here is that we are going to store patterns.  These
+   patterns look like:
+
+   TYP=<patern>
+   SORT=<pattern>
+
+   and from these patterns, we will be able to decide which tactic to
+   execute.
+
+   For hypotheses, we have a vector of 4 patterns:
+
+   HYP[TYP] HYP[SORT] CONCL[TYP] CONCL[SORT]
+
+   and for conclusions, we have 2:
+
+   CONCL[TYP] CONCL[SORT]
+
+   If the user doesn't supply some of these, they are just replaced
+   with empties.
+
+   The process of matching goes like this:
+
+   We use a discrimination net to look for matches between the pattern
+   for HYP[TOP] (CONCL[TOP]) and the type of the chosen hypothesis.
+   Then, we use this to look for the right tactic to apply, by
+   matching the rest of the slots.  Each match is tried, and if there
+   is more than one, this fact is reported, and the one with the
+   lowest priority is taken.  The priority is a parameter of the
+   tactic input.
+
+   The tactic input is an expression to hand to the
+   tactic-interpreter, and its priority.
+
+   For most tactics, the priority should be the number of subgoals
+   generated.
+
+   Matching is compatible with second-order matching of sopattern.
+
+   SYNTAX:
+
+   Hint DHyp <hyp-pattern> pri <tac-pattern>.
+
+   and
+
+   Hint DConcl <concl-pattern> pri <tac-pattern>.
+
+   The bindings at the end allow us to transfer information from the
+   patterns on terms into the patterns on tactics in a safe way - we
+   will perform second-order normalization and conversion to an AST
+   before substitution into the tactic-expression.
+
+   WARNING: The binding mechanism is NOT intended to facilitate the
+   transfer of large amounts of information from the terms to the
+   tactic.  This should be done in a special-purpose tactic.
+
+ *)
+
+(*
+
+Example : The tactic "if there is a hypothesis saying that the
+successor of some number is smaller than zero, then invert such
+hypothesis" is defined in this way:
+
+Require DHyp.
+Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1
+  [<:tactic:<Inversion $0>>].
+
+Then, the tactic is used like this:
+
+Goal (le (S O) O) -> False.
+Intro H.
+DHyp  H.
+Qed.
+
+The name "$0" refers to the matching hypothesis --in this case the
+hypothesis H.
+
+Similarly for the conclusion :
+
+Hint Destruct Conclusion equal_zero  (? = ?) 1 [<:tactic:<Reflexivity>>].
+
+Goal (plus O O)=O.
+DConcl.
+Qed.
+
+The "Discardable" option clears the hypothesis after using it.
+
+Require DHyp.
+Hint Destruct  Discardable Hypothesis less_than_zero (le (S ?) O) 1
+  [<:tactic:<Inversion $0>>].
+
+Goal (n:nat)(le (S n) O) -> False.
+Intros n H.
+DHyp  H.
+Qed.
+-- Eduardo (9/3/97 )
+
+*)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Reduction
+open Himsg
+open Proof_trees
+open Tacmach
+open Tactics
+open Clenv
+open Tactics
+open Tacticals
+open Libobject
+open Library
+open Vernacinterp
+open Pattern
+
+(* two patterns - one for the type, and one for the type of the type *)
+type destructor_pattern = {
+  d_typ: constr; 
+  d_sort: constr }
+    
+type ('a,'b) location = Hyp of 'a | Concl of 'b
+
+(* hypothesis patterns might need to do matching on the conclusion, too.
+ * conclusion-patterns only need to do matching on the hypothesis *)
+type located_destructor_pattern =
+   (* discadable , pattern for hyp, pattern for concl *)
+   (bool * destructor_pattern * destructor_pattern,
+   (* pattern for concl *)
+   destructor_pattern) location
+
+type destructor_data = {
+  d_pat : located_destructor_pattern;
+  d_pri : int;
+  d_code : Ast.act } (* should be of phylum tactic *)
+
+type t = (identifier,destructor_data) Nbtermdn.t
+type frozen_t = (identifier,destructor_data) Nbtermdn.frozen_t
+
+let tactab = (Nbtermdn.create () : t)
+
+let lookup pat = Nbtermdn.lookup tactab pat
+
+let init () = Nbtermdn.empty tactab
+
+let freeze () = Nbtermdn.freeze tactab
+let unfreeze fs = Nbtermdn.unfreeze fs tactab
+
+let rollback f x =
+  let fs = freeze() in 
+  try f x with e -> (unfreeze fs; raise e)
+
+let add (na,dd) =
+  let pat = match dd.d_pat with
+    | Hyp(_,p,_) -> p.d_typ
+    | Concl p -> p.d_typ
+  in 
+  if Nbtermdn.in_dn tactab na then begin
+    mSGNL [< 'sTR "Warning [Overriding Destructor Entry " ; 
+             'sTR (string_of_id na) ; 'sTR"]" >];
+    Nbtermdn.remap tactab na (pat,dd)
+  end else 
+    Nbtermdn.add tactab (na,(pat,dd))
+
+let _ = 
+  Summary.declare_summary "destruct-hyp-concl"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+
+let cache_dd (_,(na,dd)) =
+  try 
+    add (na,dd)
+  with _ -> 
+    anomalylabstrm "Dhyp.add"
+      [< 'sTR"The code which adds destructor hints broke;"; 'sPC; 
+	 'sTR"this is not supposed to happen" >]
+
+let specification_dd x = x
+
+type destructor_data_object = identifier * destructor_data
+
+let ((inDD:destructor_data_object->obj),
+     (outDD:obj->destructor_data_object)) =
+  declare_object ("DESTRUCT-HYP-CONCL-DATA",
+                  { load_function = (fun _ -> ());
+                    cache_function = cache_dd;
+		    open_function = (fun _ -> ());
+                    specification_function = specification_dd })
+    
+let add_destructor_hint na pat pri code =
+  Lib.add_anonymous_leaf
+    (inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
+
+let _ = 
+  vinterp_add
+    ("HintDestruct",
+     fun [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
+          VARG_NUMBER pri; VARG_AST tacexp] ->
+       let loc =
+	 match location with
+           | Node(_,"CONCL",[]) -> CONCL()
+	   | Node(_,"DiscardableHYP",[]) -> HYP true
+	   | Node(_,"PreciousHYP",[]) -> HYP false 
+       in
+       fun () ->
+	 let pat = raw_sopattern_of_compattern (initial_sign()) patcom in
+	 let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in
+	 add_destructor_hint na
+           (match loc with
+              | HYP b ->
+		  HYP(b,{d_typ=pat;d_sort=DOP0(Meta(newMETA()))},
+                      { d_typ=DOP0(Meta(newMETA()));
+		       	d_sort=DOP0(Meta(newMETA())) })
+              | CONCL () ->
+		  CONCL({d_typ=pat;d_sort=DOP0(Meta(newMETA()))}))
+           pri code)
+
+let match_dpat dp cls gls =
+  let cltyp = clause_type cls gls in
+  match (cls,dp) with
+    | (Some id,Hyp(_,hypd,concld)) ->
+        (somatch None hypd.d_typ cltyp)@
+        (somatch None hypd.d_sort (pf_type_of gls cltyp))@
+        (somatch None concld.d_typ (pf_concl gls))@
+        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+    | (None,Concl concld) ->
+        (somatch None concld.d_typ (pf_concl gls))@
+        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+    | _ -> error "ApplyDestructor"
+
+let applyDestructor cls discard dd gls =
+  let mvb = match_dpat dd.d_pat cls gls in
+  let astb = match cls with
+    | Some id -> ["$0", Vast (nvar (string_of_id id))]
+    | None -> ["$0", Vast (nvar "$0")] in
+  (* TODO: find the real location *)
+  let (Vast tcom) = Ast.eval_act dummy_loc astb dd.d_code in
+  let discard_0 =
+    match (cls,dd.d_pat) with
+      | (Some id,HYP(discardable,_,_)) ->
+          if discard & discardable then thin [id] else tclIDTAC
+      | (None,CONCL _) -> tclIDTAC
+      | _ -> error "ApplyDestructor" 
+  in
+  (tclTHEN (Tacinterp.interp tcom) discard_0) gls
+
+(* [DHyp id gls]
+
+   will take an identifier, get its type, look it up in the
+   discrimination net, get the destructors stored there, and then try
+   them in order of priority. *)
+
+let destructHyp discard id gls =
+  let hyptyp = clause_type (Some id) gls in
+  let ddl = List.map snd (lookup hyptyp) in
+  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
+  tclFIRST (List.map (applyDestructor (Some id) discard) sorted_ddl) gls
+
+let cDHyp id gls = destructHyp true id gls
+let dHyp id gls = destructHyp false id gls
+
+open Tacinterp
+
+let _ = tacinterp_add("DHyp",(fun [Identifier id] -> dHyp id))
+let _ = tacinterp_add("CDHyp",(fun [Identifier id] -> cDHyp id))
+
+(* [DConcl gls]
+
+   will take a goal, get its concl, look it up in the
+   discrimination net, get the destructors stored there, and then try
+   them in order of priority. *)
+
+let dConcl gls =
+  let ddl = List.map snd (lookup (pf_concl gls)) in
+  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
+  tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
+
+let _ = tacinterp_add("DConcl",(fun [] -> dConcl))
+
+let to2Lists (table:t) = Nbtermdn.to2Lists table
+
+let rec search n =
+  if n=0 then error "Search has reached zero.";
+  tclFIRST
+    [intros;
+     assumption;
+     (tclTHEN  
+        (Tacticals.tryAllClauses 
+           (function 
+              | Some id -> (dHyp id)
+              | None    ->  dConcl ))
+        (search (n-1)))]
+    
+let auto_tdb n = tclTRY (tclCOMPLETE (search n))
+   
+let sarch_depth_tdb = ref(5)
+			
+let dyn_auto_tdb = function 
+  | [Integer n] -> auto_tdb n 
+  | []          -> auto_tdb !sarch_depth_tdb
+
+let h_auto_tdb = hide_tactic "AutoTDB" dyn_auto_tdb
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
new file mode 100644
index 0000000000..b59df6334b
--- /dev/null
+++ b/tactics/dhyp.mli
@@ -0,0 +1,5 @@
+
+(* $Id$ *)
+
+(* Programmable destruction of hypotheses and conclusions. *)
+
diff --git a/tactics/elim.ml b/tactics/elim.ml
new file mode 100644
index 0000000000..3fe9430c8c
--- /dev/null
+++ b/tactics/elim.ml
@@ -0,0 +1,187 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Reduction
+open Proof_trees
+open Clenv
+open Pattern
+open Tacmach
+open Tacticals
+open Tactics
+open Hiddentac
+
+let introElimAssumsThen tac ba =
+  let nassums = 
+    List.fold_left 
+      (fun acc b -> if b then acc+2 else acc+1) 
+      0 ba.branchsign 
+  in 
+  let introElimAssums = tclDO nassums intro in 
+  (tclTHEN introElimAssums (elim_on_ba tac ba))
+
+let introCaseAssumsThen tac ba =
+  let case_thin_sign =
+    List.flatten 
+      (List.map 
+	 (function b -> if b then [false;true] else [false]) 
+	 ba.branchsign) 
+  in 
+  let introCaseAssums = intros_clearing case_thin_sign in
+  (tclTHEN introCaseAssums (case_on_ba tac ba))
+
+(* The following tactic Decompose repeatedly applies the
+   elimination(s) rule(s) of the types satisfying the predicate
+   ``recognizer'' onto a certain hypothesis. For example :
+
+Require Elim.
+Require Le.
+   Goal (y:nat){x:nat | (le O x)/\(le x y)}->(le O y).
+   Intros y H.
+   Decompose [sig and] H;EAuto.
+   Qed.
+
+Another example :
+
+   Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
+   Intros A B C H; Decompose [and or] H; Assumption.
+   Qed.
+*)
+
+let elimClauseThen tac idopt gl =
+  elimination_then tac ([],[]) (VAR (out_some idopt)) gl
+
+let rec general_decompose_clause recognizer =
+  ifOnClause recognizer
+    (fun cls ->
+       elimClauseThen
+	 (introElimAssumsThen
+            (fun bas ->
+               (tclTHEN (clear_clause cls)
+		  (tclMAP (general_decompose_clause recognizer) 
+		     (List.map in_some bas.assums)))))
+	 cls)
+    (fun _ -> tclIDTAC)
+
+let rec general_decompose recognizer c gl = 
+  let typc = pf_type_of gl c in  
+  (tclTHENS (cut typc) 
+     [(tclTHEN intro 
+         (onLastHyp (general_decompose_clause recognizer)));
+      (exact c)]) gl
+  
+let head_in l c = List.mem (List.hd (head_constr c)) l
+		    
+let decompose_these c l gls =
+  let l = List.map (pf_global gls) l in 
+  general_decompose (fun (_,t) -> head_in l t) c gls
+
+let decompose_nonrec c gls =
+  general_decompose 
+    (fun (_,t) -> 
+       (is_non_recursive_type  (List.hd (head_constr t))))
+    c gls
+
+let decompose_and c gls = 
+  general_decompose 
+    (fun (_,t) -> (is_conjunction (List.hd (head_constr t))))
+    c gls
+
+let decompose_or c gls = 
+  general_decompose 
+    (fun (_,t) -> (is_disjunction (List.hd (head_constr t))))
+    c gls
+
+let dyn_decompose args gl = 
+  match args with 
+    | [Clause ids; Command c] -> 
+        decompose_these (pf_constr_of_com gl c) ids gl
+    | [CLAUSE ids; Constr c]  -> 
+        decompose_these c ids  gl
+    | l -> bad_tactic_args "DecomposeThese" l gl
+	  
+let h_decompose =
+  let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in 
+  fun ids c -> v_decompose [(CLAUSE ids);(CONSTR c)] 
+
+let vernac_decompose_and = 
+  hide_constr_tactic "DecomposeAnd" decompose_and
+let vernac_decompose_or  = 
+  hide_constr_tactic  "DecomposeOr"  decompose_or
+
+(* The tactic Double performs a double induction *)
+
+let simple_elimination c gls =
+  simple_elimination_then (fun _ -> tclIDTAC) c gls
+
+let induction_trailer abs_i abs_j bargs =
+  tclTHEN 
+    (tclDO (abs_j - abs_i) intro)
+    (onLastHyp
+       (fun idopt gls ->
+	  let id = out_some idopt in
+	  let idty = pf_type_of gls (VAR id) in
+	  let fvty = global_vars idty in
+	  let possible_bring_ids =
+	    (List.tl (List.map out_some (nLastHyps (abs_j - abs_i) gls)))
+            @bargs.assums in
+	  let (ids,_) = List.fold_left 
+			  (fun (bring_ids,leave_ids) cid ->
+                             let cidty = pf_type_of gls (VAR cid) in
+                             if not (List.mem cid leave_ids)
+                             then (cid::bring_ids,leave_ids)
+                             else (bring_ids,cid::leave_ids))
+			  ([],fvty) possible_bring_ids 
+	  in 
+	  (tclTHEN (tclTHEN (bring_hyps (List.map in_some ids))
+		      (clear_clauses (List.rev (List.map in_some ids))))
+             (simple_elimination (VAR id))) gls))
+
+let double_ind abs_i abs_j gls =
+  let cl = pf_concl gls in 
+  (tclTHEN (tclDO abs_i intro)
+     (onLastHyp
+       	(fun idopt ->
+           elimination_then
+             (introElimAssumsThen (induction_trailer abs_i abs_j))
+             ([],[]) (VAR (out_some idopt))))) gls
+
+let dyn_double_ind = function
+  | [Integer i; Integer j] -> double_ind i j
+  | _ -> assert false
+
+let _ = add_tactic "DoubleInd" dyn_double_ind
+
+
+(*****************************)
+(* Decomposing introductions *)
+(*****************************)
+
+let rec intro_pattern p = 
+  let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
+  and case_last  = (tclLAST_HYP h_simplest_case) in  
+  match p with
+    | IdPat  id  -> intro_using_warning id
+    | DisjPat l  -> (tclTHEN introf
+                       (tclTHENS 
+			  (tclTHEN case_last clear_last)
+			  (List.map intro_pattern l)))
+    | ConjPat l  -> (tclTHEN introf
+                       (tclTHEN (tclTHEN  case_last clear_last)
+                          (intros_pattern l)))
+    | ListPat l  ->  intros_pattern l
+
+and intros_pattern l = tclMAP intro_pattern l
+
+let dyn_intro_pattern = function 
+  | []               -> intros
+  | [Intropattern p] -> intro_pattern p
+  | l                -> bad_tactic_args "Elim.dyn_intro_pattern" l
+
+let v_intro_pattern = hide_tactic "Intros" dyn_intro_pattern
+
+let h_intro_pattern p = v_intro_pattern [Intropattern p]
diff --git a/tactics/elim.mli b/tactics/elim.mli
new file mode 100644
index 0000000000..ee1b10a377
--- /dev/null
+++ b/tactics/elim.mli
@@ -0,0 +1,33 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Proof_trees
+open Tacmach
+open Tacticals
+(*i*)
+
+(* Eliminations tactics. *)
+
+val introElimAssumsThen :
+  (branch_assumptions -> tactic) -> branch_args -> tactic
+
+val introCaseAssumsThen :
+  (branch_assumptions -> tactic) -> branch_args -> tactic
+
+val general_decompose_clause : (clause * constr -> bool) -> clause -> tactic
+val general_decompose        : (clause * constr -> bool) -> constr -> tactic
+val decompose_nonrec         : constr -> tactic
+val decompose_and            : constr -> tactic
+val decompose_or             : constr -> tactic
+val h_decompose              : identifier list -> constr -> tactic
+
+val double_ind : int -> int -> tactic
+
+val intro_pattern     : intro_pattern      -> tactic
+val intros_pattern    : intro_pattern list -> tactic
+val dyn_intro_pattern : tactic_arg list    -> tactic
+val v_intro_pattern   : tactic_arg list    -> tactic
+val h_intro_pattern   : intro_pattern      -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 07ef757a56..049fb1e14b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,9 +6,6 @@ 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]
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 1d9b25757a..3929903644 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -9,6 +9,9 @@ open Tacmach
 open Tacentries
 (*i*)
 
+(* Tactics for the interpreter. They left a trace in the proof tree
+   when they are called. *)
+
 val h_clear           : identifier list -> tactic
 val h_move            : bool -> identifier -> identifier -> tactic
 val h_contradiction   : tactic
diff --git a/tactics/pattern.mli b/tactics/pattern.mli
index 4cfb482564..fc9d07ef7f 100644
--- a/tactics/pattern.mli
+++ b/tactics/pattern.mli
@@ -46,6 +46,7 @@ val make_module_marker : string list -> module_mark
 val put_pat            : module_mark -> string -> marked_term
 val get_pat            : marked_term -> constr
 val pattern_stock      : constr Stock.stock
+
 (*i**
 val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr
 **i*)
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index ed19fd8d82..687de4d7d1 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -6,6 +6,8 @@ open Proof_trees
 open Tacmach
 (*i*)
 
+(* Registered tactics. *)
+
 val v_absurd        : tactic_arg list -> tactic
 val v_contradiction : tactic_arg list -> tactic
 val v_reflexivity   : tactic_arg list -> tactic
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 216a24b310..298b5abd96 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -13,6 +13,8 @@ open Pattern
 open Wcclausenv
 (*i*)
 
+(* Tacticals i.e. functions from tactics to tactics. *)
+
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
@@ -38,7 +40,7 @@ val tclTRY_HYPS      : (constr -> tactic) -> tactic
 val dyn_tclIDTAC     : tactic_arg list -> tactic
 val dyn_tclFAIL      : tactic_arg list -> tactic
 
-(* Clause tacticals *)
+(*s Clause tacticals. *)
 
 type clause = identifier option
 
@@ -67,20 +69,19 @@ val onNthLastHyp   : int -> (clause -> tactic) -> tactic
 val onNLastHyps    : int -> (clause -> tactic) -> tactic
 val clauseTacThen  : (clause -> tactic) -> tactic -> clause -> tactic
 val if_tac         : (goal sigma -> bool) -> tactic -> (tactic) -> tactic
-val ifOnClause     : (clause * constr -> bool) -> 
-                      (clause -> tactic) -> 
-                      (clause -> tactic) -> 
-                       clause -> tactic
+val ifOnClause     : 
+  (clause * constr -> bool) -> (clause -> tactic) -> (clause -> tactic) -> 
+    clause -> tactic
 
-(* Usage : [ConclPattern concl pat tacast]
+(*i Usage : [ConclPattern concl pat tacast]
    if the term concl matches the pattern pat, (in sense of 
    Pattern.somatches, then replace ?1 ?2 metavars in tacast by the
    right values to build a tactic *)
 (***
 val conclPattern : constr -> constr -> CoqAst.t -> tactic
-***)
+**i*)
 
-(* Elimination tacticals *)
+(*s Elimination tacticals. *)
 
 type branch_args = { 
   ity        : constr;      (* the type we were eliminating on *)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 3cea47392d..8aee8dcb7c 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -11,6 +11,8 @@ open Tacmach
 open Clenv
 (*i*)
 
+(* A somewhat cryptic module. *)
+
 val pf_get_new_id  : identifier      -> goal sigma -> identifier
 val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 
@@ -21,8 +23,9 @@ type arg_binder =
 
 type arg_bindings = (arg_binder * constr) list
 
-val clenv_constrain_with_bindings :
-  arg_bindings -> walking_constraints clausenv -> walking_constraints clausenv
+type wc = walking_constraints
+
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
 (*i**
 val add_prod_rel : 'a evar_map -> constr * context -> constr * context
@@ -36,26 +39,22 @@ val add_prods_sign :
   'a evar_map -> constr * typed_type signature -> constr * typed_type signature
 **i*)
 
-val res_pf_THEN         : (walking_constraints -> tactic) -> 
-                           walking_constraints clausenv -> 
-                          (walking_constraints clausenv -> tactic) -> tactic
+val res_pf_THEN : 
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
+
+val res_pf_THEN_i : 
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
+    int -> tactic
 
-val res_pf_THEN_i       : (walking_constraints -> tactic) -> 
-                           walking_constraints clausenv -> 
-                          (walking_constraints clausenv -> int -> tactic) -> 
-                           int -> tactic
+val elim_res_pf_THEN_id : 
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
+    int -> tactic
 
-val elim_res_pf_THEN_i  : (walking_constraints -> tactic) -> 
-                           walking_constraints clausenv -> 
-                          (walking_constraints clausenv -> int -> tactic) -> 
-                            int -> tactic
+val mk_clenv_using : wc -> constr -> wc clausenv
 
-val mk_clenv_using      : walking_constraints -> constr -> 
-                                     walking_constraints clausenv
+val applyUsing : constr -> tactic
 
-val applyUsing          : constr -> tactic
+val clenv_apply_n_times : int -> wc clausenv -> wc clausenv
 
-val clenv_apply_n_times : int -> walking_constraints clausenv -> 
-                          walking_constraints clausenv
 
 
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 22caa2a9fa..b2509d0119 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -19,21 +19,21 @@ type input_buffer = {
   mutable tokens : Gram.parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
-(* The input buffer of stdin *)
+(* The input buffer of stdin. *)
 
 val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
   May raise only the following exceptions: [Drop] and [End_of_input],
-  meaning we get out of the Coq loop *)
+  meaning we get out of the Coq loop. *)
 
 val print_toplevel_error : exn -> std_ppcmds
 
-(* Parse and execute a vernac command *)
+(* Parse and execute a vernac command. *)
 
 val do_vernac : unit -> unit
 
-(* Main entry point of Coq: read and execute vernac commands *)
+(* Main entry point of Coq: read and execute vernac commands. *)
 
 val loop : unit -> unit