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

12 files changed, 1633 insertions, 29 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
new file mode 100644
index 000000000..634e71f99
--- /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 000000000..01a2d5f6d
--- /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 000000000..bdc0faf27
--- /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 000000000..b59df6334
--- /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 000000000..3fe9430c8
--- /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 000000000..ee1b10a37
--- /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 07ef757a5..049fb1e14 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 1d9b25757..392990364 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 4cfb48256..fc9d07ef7 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 ed19fd8d8..687de4d7d 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 216a24b31..298b5abd9 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 3cea47392..8aee8dcb7 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