- Optimized "auto decomp" which had a (presumably) exponential in

  the number of conjunctions to split.
- A few cleaning and uniformisation in auto.ml.
- Removal of v62 hints already in core.


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

14 files changed, 223 insertions, 181 deletions

diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f6ebcae66..182351427 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,6 +137,7 @@ exception FailError of int * Pp.std_ppcmds
    level or do nothing. *)
 val catch_failerror  : exn -> unit
 
+val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclREPEAT_MAIN   : tactic -> tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index aa7ce1290..b1e669388 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,6 +117,19 @@ let is_transparent_gr (ids, csts) = function
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
       
+let fmt_autotactic =
+  function
+  | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
+  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
+  | Give_exact c -> (str"exact " ++ pr_lconstr c)
+  | Res_pf_THEN_trivial_fail (c,clenv) -> 
+      (str"apply " ++ pr_lconstr c ++ str" ; trivial")
+  | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
+  | Extern tac -> 
+      (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
+
+let pr_autotactic = fmt_autotactic
+
 module Hint_db = struct
 
   type t = { 
@@ -580,7 +593,7 @@ let add_hints local dbnames0 h =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let fmt_autotactic =
+let pr_autotactic =
   function
   | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
   | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
@@ -591,19 +604,19 @@ let fmt_autotactic =
   | Extern tac -> 
       (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
 
-let fmt_hint v =
-  (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
+let pr_hint v =
+  (pr_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
 
-let fmt_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist fmt_hint hintlist) ++ fnl ())
+let pr_hint_list hintlist =
+  (str "  " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
 
-let fmt_hints_db (name,db,hintlist) =
+let pr_hints_db (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
      if hintlist = [] then (str " nothing" ++ fnl ())
-     else (fnl () ++ fmt_hint_list hintlist))
+     else (fnl () ++ pr_hint_list hintlist))
 
 (* Print all hints associated to head c in any database *)
-let fmt_hint_list_for_head c = 
+let pr_hint_list_for_head c = 
   let dbs = Hintdbmap.to_list !searchtable in
   let valid_dbs = 
     map_succeed 
@@ -615,14 +628,14 @@ let fmt_hint_list_for_head c =
   else 
     hov 0 
       (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
-	 hov 0 (prlist fmt_hints_db valid_dbs))
+	 hov 0 (prlist pr_hints_db valid_dbs))
 
-let fmt_hint_ref ref = fmt_hint_list_for_head ref
+let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
-let print_hint_ref ref =  ppnl(fmt_hint_ref ref)
+let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
-let fmt_hint_term cl = 
+let pr_hint_term cl = 
   try 
     let (hdc,args) = match head_constr_bound cl [] with 
       | hdc::args -> (hdc,args)
@@ -645,14 +658,14 @@ let fmt_hint_term cl =
       (str "No hint applicable for current goal")
     else
       (str "Applicable Hints :" ++ fnl () ++
-	 hov 0 (prlist fmt_hints_db valid_dbs))
+	 hov 0 (prlist pr_hints_db valid_dbs))
   with Bound | Match_failure _ | Failure _ -> 
     (str "No hint applicable for current goal")
 
 let error_no_such_hint_database x =
   error ("No such Hint database: "^x^".")
 	  
-let print_hint_term cl = ppnl (fmt_hint_term cl)
+let print_hint_term cl = ppnl (pr_hint_term cl)
 
 (* print all hints that apply to the concl of the current goal *)
 let print_applicable_hint () = 
@@ -672,11 +685,11 @@ let print_hint_db db =
       | Some head ->
 	  msg (hov 0 
 		  (str "For " ++ pr_global head ++ str " -> " ++
-		      fmt_hint_list hintlist))
+		      pr_hint_list hintlist))
       | None ->
 	  msg (hov 0 
 		  (str "For any goal -> " ++
-		      fmt_hint_list hintlist)))
+		      pr_hint_list hintlist)))
     db
 
 let print_hint_db_by_name dbname =
@@ -701,7 +714,10 @@ let print_searchtable () =
 (*          tactics with a trace mechanism for automatic search           *)
 (**************************************************************************)
 
-let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
+let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l
+
+let select_unfold_extern =
+  List.filter (function (_,{code = (Unfold_nth _ | Extern _)}) -> true | _ -> false)
 
 (* tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds oftener) *)
@@ -716,25 +732,33 @@ let auto_unif_flags = {
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve_nodelta (c,clenv) gls = 
-  let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in  
-  h_simplest_apply c gls
+let unify_resolve_nodelta (c,clenv) gl = 
+  let clenv' = connect_clenv gl clenv in
+  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in  
+  h_simplest_apply c gl
 
-let unify_resolve flags (c,clenv) gls = 
-  let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false ~flags clenv' gls in  
-  h_apply true false [inj_open c,NoBindings] gls
+let unify_resolve flags (c,clenv) gl = 
+  let clenv' = connect_clenv gl clenv in
+  let _ = clenv_unique_resolver false ~flags clenv' gl in  
+  h_apply true false [inj_open c,NoBindings] gl
 
+let unify_resolve_gen = function
+  | None -> unify_resolve_nodelta
+  | Some flags -> unify_resolve flags
 
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
-let make_local_hint_db eapply lems g =
-  let sign = pf_hyps g in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in
-  let hintlist' = list_map_append (pf_apply make_resolves g (eapply,true,false) None) lems in
-    Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false))
+let add_hint_lemmas eapply lems hint_db gl =
+  let hintlist' = 
+    list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
+  Hint_db.add_list hintlist' hint_db
+
+let make_local_hint_db eapply lems gl =
+  let sign = pf_hyps gl in
+  let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
+  add_hint_lemmas eapply lems
+    (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false)) gl
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
    substitution sans passer par bdize dont l'objectif est de préparer un
@@ -787,29 +811,12 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
        (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
 
 and my_find_search_nodelta db_list local_db hdc concl =
-  let tacl = 
-    if occur_existential concl then 
-      list_map_append (Hint_db.map_all hdc)
-	(local_db::db_list)
-    else
-      list_map_append (Hint_db.map_auto (hdc,concl))
-      	(local_db::db_list)
-  in
-    List.map 
-      (fun {pri=b; pat=p; code=t} -> 
-	(b,
-	match t with
-	  | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl)
-	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
-	  | Give_exact c  -> exact_check c
-	  | Res_pf_THEN_trivial_fail (term,cl) -> 
-	      tclTHEN 
-		(unify_resolve_nodelta (term,cl)) 
-		(trivial_fail_db false db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
-	  | Extern tacast -> 
-	      conclPattern concl p tacast))
-    tacl
+  if occur_existential concl then
+    List.map (fun hint -> (None,hint))
+      (list_map_append (Hint_db.map_all hdc) (local_db::db_list))
+  else
+    List.map (fun hint -> (None,hint))
+      (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
@@ -817,54 +824,51 @@ and my_find_search mod_delta =
     
 and my_find_search_delta db_list local_db hdc concl =
   let flags = {auto_unif_flags with use_metas_eagerly = true} in
-  let tacl = 
     if occur_existential concl then 
       list_map_append
 	(fun db -> 
 	  if Hint_db.use_dn db then 
 	    let flags = flags_of_state (Hint_db.transparent_state db) in
-	      List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	      List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
 	  else
-	    let st = {flags with modulo_delta = Hint_db.transparent_state db} in
-	      List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+	    let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
+	      List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db))
 	(local_db::db_list)
     else
       list_map_append (fun db -> 
 	if Hint_db.use_dn db then 
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
-	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	    List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
 	else
 	  let (ids, csts as st) = Hint_db.transparent_state db in
-	  let st, l = 
+	  let flags, l =
 	    let l =
 	      if (Idpred.is_empty ids && Cpred.is_empty csts)
 	      then Hint_db.map_auto (hdc,concl) db
 	      else Hint_db.map_all hdc db
 	    in {flags with modulo_delta = st}, l
-	  in List.map (fun x -> (st,x)) l)
+	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
-  in
-    List.map 
-      (fun (st, {pri=b; pat=p; code=t}) -> 
-	(b,
-	match t with
-	  | Res_pf (term,cl) -> unify_resolve st (term,cl)
-	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
-	  | Give_exact c  -> exact_check c
-	  | Res_pf_THEN_trivial_fail (term,cl) -> 
-	      tclTHEN 
-		(unify_resolve st (term,cl)) 
-		(trivial_fail_db true db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
-	  | Extern tacast -> 
-	      conclPattern concl p tacast))
-      tacl
+
+and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
+  match t with
+  | Res_pf (term,cl) -> unify_resolve_gen flags (term,cl)
+  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
+  | Give_exact c  -> exact_check c
+  | Res_pf_THEN_trivial_fail (term,cl) -> 
+      tclTHEN 
+        (unify_resolve_gen flags (term,cl))
+        (trivial_fail_db (flags <> None) db_list local_db)
+  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+  | Extern tacast -> conclPattern concl p tacast
       
 and trivial_resolve mod_delta db_list local_db cl = 
   try 
     let hdconstr = List.hd (head_constr_bound cl []) in
-    priority 
-      (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl)
+    List.map (tac_of_hint db_list local_db cl)
+      (priority 
+	(my_find_search mod_delta db_list local_db
+	  (head_of_constr_reference hdconstr) cl))
   with Bound | Not_found -> 
     []
 
@@ -903,69 +907,80 @@ let h_trivial lems l =
 let possible_resolve mod_delta db_list local_db cl =
   try 
     let hdconstr = List.hd (head_constr_bound cl []) in
-    List.map snd 
-      (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl)
+    List.map (tac_of_hint db_list local_db cl)
+      (my_find_search mod_delta db_list local_db
+        (head_of_constr_reference hdconstr) 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 Hipattern.is_conjunction hd then 
-    simplest_case c gls 
-  else 
-    errorlabstrm "Auto.decomp_unary_term" (str "Not a unary type.")
+let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
+  try
+    let hd = List.hd (head_constr typc) in 
+    match Hipattern.match_with_conjunction_size hd with
+    | Some (_,_,n) -> tclTHEN (simplest_case (mkVar id)) (kont1 n) gl
+    | None -> kont2 gl
+  with UserError _ -> kont2 gl
 
-let decomp_empty_term c gls = 
-  let typc = pf_type_of gls c in 
+let decomp_empty_term (id,_,typc) gl = 
   let (hd,_) = decompose_app typc in 
   if Hipattern.is_empty_type hd then 
-    simplest_case c gls 
+    simplest_case (mkVar id) gl 
   else 
     errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
 
+let extend_local_db gl decl db =
+  Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
+
+(* Try to decompose hypothesis [decl] into atomic components of a 
+   conjunction with maximum depth [p] (or solve the goal from an 
+   empty type) then call the continuation tactic with hint db extended 
+   with the obtappined not-further-decomposable hypotheses *)
+
+let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl =
+  if p = 0 then
+    kont (extend_local_db gl decl db) gl
+  else
+    tclORELSE0
+      (decomp_empty_term decl)
+      (decomp_unary_term_then decl (intros_decomp (p-1) kont [] db)
+	(kont (extend_local_db gl decl db))) gl
+
+(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
+   call the continuation tactic [kont] with the hint db extended
+   with the so-obtained not-further-decomposable hypotheses *)
+
+and intros_decomp p kont decls db n =
+  if n = 0 then
+    decomp_and_register_decls p kont decls db
+  else
+    tclTHEN intro (tclLAST_DECL (fun d ->
+      (intros_decomp p kont (d::decls) db (n-1))))
+
+(* Decompose hypotheses [hyps] with maximum depth [p] and
+   call the continuation tactic [kont] with the hint db extended
+   with the so-obtained not-further-decomposable hypotheses *)
+
+and decomp_and_register_decls p kont decls =
+  List.fold_left (decomp_and_register_decl p) kont decls
+
 
 (* 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 mod_delta db_list local_db extra_sign goal =
-  if n=0 then error "BOUND 2";
-  let decomp_tacs = match decomp with 
-    | 0 -> [] 
-    | p -> 
-	(tclTRY_sign decomp_empty_term extra_sign)
-	::
-	(List.map 
-	   (fun id -> tclTHENSEQ
-               [decomp_unary_term (mkVar id);
-                clear [id];
-		search_gen decomp p mod_delta db_list local_db []])
-	   (pf_ids_of_hyps goal)) 
-  in
-  let intro_tac = 
-    tclTHEN intro 
-      (fun g' -> 
-	 let (hid,_,htyp as d) = pf_last_hyp g' in
-	 let hintl = 
-	   try 
-	     [make_apply_entry (pf_env g') (project g')
-		(true,true,false) None
-		(mkVar hid, htyp)]
-	   with Failure _ -> [] 
-	 in
-         search_gen decomp n mod_delta db_list (Hint_db.add_list hintl local_db) [d] g') 
-  in
-  let rec_tacs = 
-    List.map 
-      (fun ntac -> 
-	 tclTHEN ntac
-	   (search_gen decomp (n-1) mod_delta db_list local_db empty_named_context))
-      (possible_resolve mod_delta db_list local_db (pf_concl goal))
-  in 
-  tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
+exception Uplift of tactic list
 
+let rec search_gen p n mod_delta db_list local_db =
+  let rec search n local_db gl =
+    if n=0 then error "BOUND 2";
+    tclFIRST
+      (assumption ::
+       intros_decomp p (search n) [] local_db 1 ::
+       List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db)) 
+	(possible_resolve mod_delta db_list local_db (pf_concl gl))) gl
+  in
+  search n local_db
 
 let search = search_gen 0
 
@@ -981,8 +996,7 @@ let delta_auto mod_delta n lems dbnames gl =
 	   error_no_such_hint_database x)
       ("core"::dbnames) 
   in
-  let hyps = pf_hyps gl in
-  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl
+  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
 let auto = delta_auto false
 
@@ -994,8 +1008,7 @@ let delta_full_auto mod_delta n lems gl =
   let dbnames = Hintdbmap.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_hyps gl in
-  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl
+  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
 let full_auto = delta_full_auto false
 let new_full_auto = delta_full_auto true
@@ -1020,14 +1033,15 @@ let h_auto n lems l =
 
 (* 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 lems n gl = 
-  let hyps = pf_hyps gl in
-  search_gen des_opt n false (List.map searchtable_map ["core";"extcore"])
-    (make_local_hint_db false lems gl) hyps gl
+let default_search_decomp = ref 20
+
+let destruct_auto p lems n gl = 
+  decomp_and_register_decls p (fun local_db gl ->
+    search_gen p n false (List.map searchtable_map ["core";"extcore"])
+      (add_hint_lemmas false lems local_db gl) gl)
+    (pf_hyps gl)
+    (Hint_db.empty empty_transparent_state false)
+    gl
     
 let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
 
@@ -1086,25 +1100,23 @@ let compileAutoArg contac = function
 
 let compileAutoArgList contac = List.map (compileAutoArg contac)
 
-let rec super_search n db_list local_db argl goal =
+let rec super_search n db_list local_db argl gl =
   if n = 0 then error "BOUND 2";
   tclFIRST
     (assumption
      ::
-     (tclTHEN intro 
+     tclTHEN intro 
         (fun g -> 
 	   let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in
 	   super_search n db_list (Hint_db.add_list hintl local_db)
-	     argl g))
+	     argl g)
      ::
-     ((List.map 
-         (fun ntac -> 
+     List.map (fun ntac -> 
             tclTHEN ntac 
               (super_search (n-1) db_list local_db argl))
-         (possible_resolve false db_list local_db (pf_concl goal)))
+         (possible_resolve false db_list local_db (pf_concl gl))
       @
-      (compileAutoArgList  
-         (super_search (n-1) db_list local_db argl) argl))) goal
+      compileAutoArgList (super_search (n-1) db_list local_db argl) argl) gl
 
 let search_superauto n to_add argl g = 
   let sigma =
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0eaa35872..1f72f365a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -150,7 +150,7 @@ val set_extern_subst_tactic :
 
 val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
 
-val priority : (int * 'a) list -> 'a list
+val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
 
 val default_search_depth : int ref
 
@@ -202,7 +202,7 @@ val gen_trivial : constr list -> hint_db_name list option -> tactic
 val full_trivial : constr list -> tactic
 val h_trivial : constr list -> hint_db_name list option -> tactic
 
-val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
+val pr_autotactic : auto_tactic -> Pp.std_ppcmds
 
 (*s The following is not yet up to date -- Papageno. *)
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 001ae0315..347128921 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -139,7 +139,7 @@ and e_my_find_search db_list local_db hdc concl =
 	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	  | Extern tacast -> conclPattern concl p tacast
       in 
-	(tac,b,fmt_autotactic t)
+	(tac,b,pr_autotactic t)
   in 
     List.map tac_of_hint hintl
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5610f7518..dd51acc7b 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -91,6 +91,8 @@ open Unification
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
+let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
+
 (* no delta yet *)
 
 let unify_e_resolve flags (c,clenv) gls = 
@@ -142,9 +144,9 @@ and e_my_find_search_nodelta db_list local_db hdc concl =
 	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> conclPattern concl p tacast
        in 
-       (tac,fmt_autotactic t))
+       (tac,pr_autotactic t))
        (*i
-	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+	 fun gls -> pPNL (pr_autotactic t); Format.print_flush (); 
                      try tac gls
 		     with e when Logic.catchable_exception(e) -> 
                             (Format.print_string "Fail\n"; 
@@ -180,9 +182,9 @@ and e_my_find_search_delta db_list local_db hdc concl =
 	   | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
 	   | Extern tacast -> conclPattern concl p tacast
        in 
-       (tac,fmt_autotactic t))
+       (tac,pr_autotactic t))
        (*i
-	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+	 fun gls -> pPNL (pr_autotactic t); Format.print_flush (); 
                      try tac gls
 		     with e when Logic.catchable_exception(e) -> 
                             (Format.print_string "Fail\n"; 
@@ -194,7 +196,7 @@ and e_my_find_search_delta db_list local_db hdc concl =
     
 and e_trivial_resolve mod_delta db_list local_db gl = 
   try 
-    Auto.priority 
+    priority 
       (e_my_find_search mod_delta db_list local_db 
 	 (List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 9e0281855..c796eda90 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -67,7 +67,7 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 (* A general conjunction type is a non-recursive inductive type with
    only one constructor. *)
 
-let match_with_conjunction t =
+let match_with_conjunction_size t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
     | Ind ind -> 
@@ -76,11 +76,16 @@ let match_with_conjunction t =
 	  && (not (mis_is_recursive (ind,mib,mip)))
           && (mip.mind_nrealargs = 0)
         then 
-	  Some (hdapp,args)
+	  Some (hdapp,args,mip.mind_consnrealdecls.(0))
         else 
 	  None
     | _ -> None
 
+let match_with_conjunction t =
+  match match_with_conjunction_size t with
+  | Some (hd,args,n) -> Some (hd,args)
+  | None -> None
+
 let is_conjunction t = op2bool (match_with_conjunction t)
     
 (* A general disjunction type is a non-recursive inductive type all
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index ce1c70e5a..a97891c14 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -56,6 +56,7 @@ val match_with_disjunction : (constr * constr list) matching_function
 val is_disjunction         : testing_function 
 
 val match_with_conjunction : (constr * constr list) matching_function
+val match_with_conjunction_size : (constr * constr list * int) matching_function
 val is_conjunction         : testing_function 
 
 val match_with_empty_type  : constr matching_function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1e4f6a050..73e7fe16e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -41,6 +41,7 @@ open Tacexpr
 let tclNORMEVAR      = tclNORMEVAR
 let tclIDTAC         = tclIDTAC
 let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
+let tclORELSE0       = tclORELSE0
 let tclORELSE        = tclORELSE
 let tclTHEN          = tclTHEN
 let tclTHENLIST      = tclTHENLIST
@@ -75,7 +76,7 @@ let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
 let unTAC            = unTAC
 
 (* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
-let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
+let tclTHENSEQ = tclTHENLIST
 
 (* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
 (* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
@@ -88,10 +89,16 @@ let tclNTH_HYP m (tac : constr->tactic) gl =
   tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
        with Failure _ -> error "No such assumption.") gl
 
+let tclNTH_DECL m tac gl =
+  tac (try List.nth (pf_hyps gl) (m-1) 
+       with Failure _ -> error "No such assumption.") gl
+
 (* apply a tactic to the last element of the signature  *)
 
 let tclLAST_HYP = tclNTH_HYP 1
 
+let tclLAST_DECL = tclNTH_DECL 1
+
 let tclLAST_NHYPS n tac gl =
   tac (try list_firstn n (pf_ids_of_hyps gl)
        with Failure _ -> error "No such assumptions.") gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 8cc556c62..00ce4da8d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -28,6 +28,7 @@ open Tacexpr
 val tclNORMEVAR      : tactic
 val tclIDTAC         : tactic
 val tclIDTAC_MESSAGE : std_ppcmds -> tactic
+val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENSEQ       : tactic list -> tactic
@@ -57,8 +58,10 @@ val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 
 val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
+val tclNTH_DECL      : int -> (named_declaration -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 val tclLAST_HYP      : (constr -> tactic) -> tactic
+val tclLAST_DECL     : (named_declaration -> tactic) -> tactic
 val tclLAST_NHYPS    : int -> (identifier list -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
new file mode 100644
index 000000000..8916b1044
--- /dev/null
+++ b/test-suite/complexity/autodecomp.v
@@ -0,0 +1,11 @@
+(* This example used to be in (at least) exponential time in the number of
+   conjunctive types in the hypotheses before revision 11713 *)
+(* Expected time < 1.50s *)
+
+Goal
+True/\True->
+True/\True->
+True/\True->
+False/\False.
+
+Time auto decomp.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index beda128af..cb96f3f60 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -59,14 +59,14 @@ Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
 Proof.
   destruct a; destruct b; intros; split; try (reflexivity || discriminate).
 Qed.
-Hint Resolve andb_prop: bool v62.
+Hint Resolve andb_prop: bool.
 
 Lemma andb_true_intro :
   forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
-Hint Resolve andb_true_intro: bool v62.
+Hint Resolve andb_true_intro: bool.
 
 (** Interpretation of booleans as propositions *)
 
@@ -115,7 +115,7 @@ Inductive Empty_set : Set :=.
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
   refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core v62.
+Hint Resolve refl_identity: core.
 
 Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
@@ -164,7 +164,7 @@ Section projections.
                               end.
 End projections. 
 
-Hint Resolve pair inl inr: core v62.
+Hint Resolve pair inl inr: core.
 
 Lemma surjective_pairing :
   forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 3667c4eb0..b01b80630 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -245,8 +245,8 @@ Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
 
-Hint Resolve I conj or_introl or_intror refl_equal: core v62.
-Hint Resolve ex_intro ex_intro2: core v62.
+Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
 
@@ -339,7 +339,7 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Hint Immediate sym_eq sym_not_eq: core v62.
+Hint Immediate sym_eq sym_not_eq: core.
 
 (** Basic definitions about relations and properties *)
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8a5b195d1..322a25468 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -59,13 +59,13 @@ Proof.
   rewrite Sn_eq_Sm; trivial.
 Qed.
 
-Hint Immediate eq_add_S: core v62.
+Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
   red in |- *; auto.
 Qed.
-Hint Resolve not_eq_S: core v62.
+Hint Resolve not_eq_S: core.
 
 Definition IsSucc (n:nat) : Prop :=
   match n with
@@ -80,13 +80,13 @@ Proof.
   unfold not; intros n H.
   inversion H.
 Qed.
-Hint Resolve O_S: core v62.
+Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
   induction n; auto.
 Qed.
-Hint Resolve n_Sn: core v62.
+Hint Resolve n_Sn: core.
 
 (** Addition *)
 
@@ -105,7 +105,7 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
   induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve plus_n_O: core v62.
+Hint Resolve plus_n_O: core.
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
 Proof.
@@ -116,7 +116,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
   intros n m; induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve plus_n_Sm: core v62.
+Hint Resolve plus_n_Sm: core.
 
 Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
 Proof.
@@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) {struct n} : nat :=
 
 where "n * m" := (mult n m) : nat_scope.
 
-Hint Resolve (f_equal2 mult): core v62.
+Hint Resolve (f_equal2 mult): core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
   induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve mult_n_O: core v62.
+Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
@@ -152,7 +152,7 @@ Proof.
   destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
   pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
 Qed.
-Hint Resolve mult_n_Sm: core v62.
+Hint Resolve mult_n_Sm: core.
 
 (** Standard associated names *)
 
@@ -179,21 +179,21 @@ Inductive le (n:nat) : nat -> Prop :=
 
 where "n <= m" := (le n m) : nat_scope.
 
-Hint Constructors le: core v62.
-(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
+Hint Constructors le: core.
+(*i equivalent to : "Hints Resolve le_n le_S : core." i*)
 
 Definition lt (n m:nat) := S n <= m.
-Hint Unfold lt: core v62.
+Hint Unfold lt: core.
 
 Infix "<" := lt : nat_scope.
 
 Definition ge (n m:nat) := m <= n.
-Hint Unfold ge: core v62.
+Hint Unfold ge: core.
 
 Infix ">=" := ge : nat_scope.
 
 Definition gt (n m:nat) := m < n.
-Hint Unfold gt: core v62.
+Hint Unfold gt: core.
 
 Infix ">" := gt : nat_scope.
 
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index b457a55b9..74d9726a6 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -53,7 +53,7 @@ Section Dependent_Equality.
 
   Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
     eq_dep_intro : eq_dep p x p x.
-  Hint Constructors eq_dep: core v62.
+  Hint Constructors eq_dep: core.
 
   Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
   Proof eq_dep_intro.
@@ -63,7 +63,7 @@ Section Dependent_Equality.
   Proof.
     destruct 1; auto.
   Qed.
-  Hint Immediate eq_dep_sym: core v62.
+  Hint Immediate eq_dep_sym: core.
 
   Lemma eq_dep_trans :
     forall (p q r:U) (x:P p) (y:P q) (z:P r),
@@ -135,8 +135,8 @@ Qed.
 
 (** Exported hints *)
 
-Hint Resolve eq_dep_intro: core v62.
-Hint Immediate eq_dep_sym: core v62.
+Hint Resolve eq_dep_intro: core.
+Hint Immediate eq_dep_sym: core.
 
 (************************************************************************)
 (** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K          *)