Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 341 insertions, 233 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 066ed786..1212656b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
 
 open Pp
 open Util
@@ -59,6 +59,8 @@ type pri_auto_tactic = {
   code : auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
+type hint_entry = global_reference option * pri_auto_tactic
+
 let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2
 
 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2
@@ -110,34 +112,60 @@ module Constr_map = Map.Make(struct
 			       let compare = Pervasives.compare 
 			     end)
 
+let is_transparent_gr (ids, csts) = function
+  | VarRef id -> Idpred.mem id ids
+  | 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 = { 
     hintdb_state : Names.transparent_state;
     use_dn : bool;
-    hintdb_map : search_entry Constr_map.t
+    hintdb_map : search_entry Constr_map.t;
+    (* A list of unindexed entries starting with an unfoldable constant
+       or with no associated pattern. *)
+    hintdb_nopat : stored_data list
   }
 
-  let empty use_dn = { hintdb_state = empty_transparent_state;
-		       use_dn = use_dn;
-		       hintdb_map = Constr_map.empty }
+  let empty st use_dn = { hintdb_state = st;
+			  use_dn = use_dn;
+			  hintdb_map = Constr_map.empty;
+			  hintdb_nopat = [] }
     
   let find key db =
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
-
+      
   let map_all k db =
     let (l,l',_) = find k db in
-      Sort.merge pri_order l l'
+      Sort.merge pri_order (db.hintdb_nopat @ l) l'
    
   let map_auto (k,c) db =
     let st = if db.use_dn then Some db.hintdb_state else None in
-      lookup_tacs (k,c) st (find k db)
-
+    let l' = lookup_tacs (k,c) st (find k db) in
+      Sort.merge pri_order db.hintdb_nopat l'
+	
   let is_exact = function 
     | Give_exact _ -> true
     | _ -> false
 
+  let rebuild_db st' db = 
+    { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map }
+
   let add_one (k,v) db =
     let st',rebuild =
       match v.code with
@@ -148,27 +176,43 @@ module Hint_db = struct
 	    | EvalConstRef cst -> (ids, Cpred.add cst csts)), true
       | _ -> db.hintdb_state, false
     in
-    let dnst, db = 
-      if db.use_dn then 
-	Some st', { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map }
-      else None, db
+    let dnst, db, k =
+      if db.use_dn then
+	let db', k' = 
+	  if rebuild then rebuild_db st' db, k
+	  else (* not an unfold *)
+	    (match k with
+	    | Some gr -> db, if is_transparent_gr st' gr then None else k
+	    | None -> db, None)
+	in
+	  (Some st', db', k')
+      else None, db, k
     in
-    let oval = find k db in
     let pat = if not db.use_dn && is_exact v.code then None else v.pat in
-      { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map;
-	hintdb_state = st' }
+      match k with
+      | None ->
+	  if not (List.mem v db.hintdb_nopat) then
+	    { db with hintdb_nopat = v :: db.hintdb_nopat }
+	  else db
+      | Some gr ->
+	  let oval = find gr db in
+	    { db with hintdb_map = Constr_map.add gr (add_tac pat v dnst oval) db.hintdb_map;
+	      hintdb_state = st' }
 	
   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.hintdb_map
+  let iter f db = 
+    f None db.hintdb_nopat;
+    Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map
     
   let transparent_state db = db.hintdb_state
 
-  let set_transparent_state db st = { db with hintdb_state = st }
+  let set_transparent_state db st =
+    let db = if db.use_dn then rebuild_db st db else db in
+      { db with hintdb_state = st }
 
-  let set_rigid db cst = 
-    let (ids,csts) = db.hintdb_state in
-      { db with hintdb_state = (ids, Cpred.remove cst csts) }
+  let use_dn db = db.use_dn
+	
 end
 
 module Hintdbmap = Gmap
@@ -235,21 +279,21 @@ let make_exact_entry pri (c,cty) =
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
-	(head_of_constr_reference (List.hd (head_constr cty)),
+	(Some (head_of_constr_reference (fst (head_constr cty))),
 	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
-let make_apply_entry env sigma (eapply,verbose) pri (c,cty) =
-  let cty = hnf_constr env sigma cty in
-  match kind_of_term cty with
+let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
+  let cty = if hnf then hnf_constr env sigma cty else cty in
+    match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
-                  with BoundPattern -> failwith "make_apply_entry") in
+          with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = List.length (clenv_missing ce) in
 	if nmiss = 0 then 
-	  (hd,
+	  (Some hd,
           { pri = (match pri with None -> nb_hyp cty | Some p -> p);
             pat = Some pat;
             code = Res_pf(c,{ce with env=empty_env}) })
@@ -258,14 +302,14 @@ let make_apply_entry env sigma (eapply,verbose) pri (c,cty) =
           if verbose then
 	    warn (str "the hint: eapply " ++ pr_lconstr c ++
 	    str " will only be used by eauto");
-          (hd,
+          (Some hd,
             { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
               pat = Some pat;
               code = ERes_pf(c,{ce with env=empty_env}) })
         end
     | _ -> failwith "make_apply_entry"
  
-(* flags is (e,v) with e=true if eapply and v=true if verbose 
+(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose 
    c is a constr
    cty is the type of constr *)
 
@@ -279,14 +323,14 @@ let make_resolves env sigma flags pri c =
   if ents = [] then
     errorlabstrm "Hint" 
       (pr_lconstr c ++ spc() ++ 
-        (if fst flags then str"cannot be used as a hint."
+        (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
 
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma (hname,_,htyp) = 
   try
-    [make_apply_entry env sigma (true, false) None
+    [make_apply_entry env sigma (true, true, false) None
        (mkVar hname, htyp)]
   with 
     | Failure _ -> []
@@ -294,23 +338,23 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
 
 (* REM : in most cases hintname = id *)
 let make_unfold (ref, eref) =
-  (ref,
+  (Some ref,
    { pri = 4;
      pat = None;
      code = Unfold_nth eref })
 
 let make_extern pri pat tacast = 
-  let hdconstr = try_head_pattern pat in 
+  let hdconstr = Option.map try_head_pattern pat in 
   (hdconstr,
    { pri=pri;
-     pat = Some pat;
+     pat = pat;
      code= Extern tacast })
 
 let make_trivial env sigma c =
   let t = hnf_constr env sigma (type_of env sigma c) in
-  let hd = head_of_constr_reference (List.hd (head_constr t)) in
+  let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
-  (hd, { pri=1;
+  (Some hd, { pri=1;
          pat = Some (Pattern.pattern_of_constr (clenv_type ce));
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
@@ -328,15 +372,29 @@ let add_hint dbname hintlist =
     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 false) in
+    let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in
     searchtable_add (dbname,db)
 
-type hint_action = CreateDB of bool | UpdateDB of (global_reference * pri_auto_tactic) list
+let add_transparency dbname grs b =
+  let db = searchtable_map dbname in
+  let st = Hint_db.transparent_state db in
+  let st' = 
+    List.fold_left (fun (ids, csts) gr -> 
+      match gr with
+      | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
+      | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts)
+      st grs
+  in searchtable_add (dbname, Hint_db.set_transparent_state db st')
+    
+type hint_action = | CreateDB of bool * transparent_state
+		   | AddTransparency of evaluable_global_reference list * bool
+		   | AddTactic of (global_reference option * pri_auto_tactic) list
 
 let cache_autohint (_,(local,name,hints)) = 
   match hints with
-  | CreateDB b -> searchtable_add (name, Hint_db.empty b)
-  | UpdateDB hints -> add_hint name hints
+  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
+  | AddTransparency (grs, b) -> add_transparency name grs b
+  | AddTactic hints -> add_hint name hints
 
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -351,11 +409,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
 	code = code ;
     }
   in
-  let subst_hint (lab,data as hint) =
-    let lab',elab' = subst_global subst lab in
-    let lab' =
-     try head_of_constr_reference (List.hd (head_constr_bound elab' []))
-     with Tactics.Bound -> lab' in
+  let subst_key gr =
+    let (lab'', elab') = subst_global subst gr in
+    let gr' = 
+      (try head_of_constr_reference (fst (head_constr_bound elab'))
+       with Tactics.Bound -> lab'')
+    in if gr' == gr then gr else gr'
+  in
+  let subst_hint (k,data as hint) =
+    let k' = Option.smartmap subst_key k in
     let data' = match data.code with
       | Res_pf (c, clenv) ->
 	  let c' = subst_mps subst c in
@@ -383,18 +445,21 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
 	    if tac==tac' then data else
 	      trans_data data (Extern tac')
     in
-      if lab' == lab && data' == data then hint else
-	(lab',data')
+      if k' == k && data' == data then hint else
+	(k',data')
   in
     match hintlist with
     | CreateDB _ -> obj
-    | UpdateDB hintlist ->
+    | AddTransparency (grs, b) -> 
+	let grs' = list_smartmap (subst_evaluable_reference subst) grs in
+	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
+    | AddTactic hintlist ->
 	let hintlist' = list_smartmap subst_hint hintlist in
 	  if hintlist' == hintlist then obj else
-	    (local,name,UpdateDB hintlist')
+	    (local,name,AddTactic hintlist')
 	      
 let classify_autohint (_,((local,name,hintlist) as obj)) =
-  if local or hintlist = (UpdateDB []) then Dispose else Substitute obj
+  if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
 let export_autohint ((local,name,hintlist) as obj) =
   if local then None else Some obj
@@ -408,8 +473,8 @@ let (inAutoHint,outAutoHint) =
                     export_function = export_autohint }
 
 
-let create_hint_db l n b = 
-  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB b))
+let create_hint_db l n st b = 
+  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
       
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
@@ -419,29 +484,40 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (local,dbname, UpdateDB
-     	      (List.flatten (List.map (fun (x, y) ->
-		make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))))
+	    (local,dbname, AddTactic
+     	      (List.flatten (List.map (fun (x, hnf, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist)))))
     dbnames
 
 
 let add_unfolds l local dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (local,dbname, UpdateDB (List.map make_unfold l))))
+       (inAutoHint (local,dbname, AddTactic (List.map make_unfold l))))
+    dbnames
+
+let add_transparency l b local dbnames =
+  List.iter 
+    (fun dbname -> Lib.add_anonymous_leaf 
+       (inAutoHint (local,dbname, AddTransparency (l, b))))
     dbnames
 
-let add_extern pri (patmetas,pat) tacast local dbname =
+let add_extern pri pat tacast local dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
   let tacmetas = [] in
-  match (list_subtract tacmetas patmetas) with
-    | i::_ ->
-	errorlabstrm "add_extern" 
-	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.")
-    | []  ->
+    match pat with
+    | Some (patmetas,pat) ->
+	(match (list_subtract tacmetas patmetas) with
+	| i::_ ->
+	    errorlabstrm "add_extern" 
+	      (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.")
+	| []  ->
+	    Lib.add_anonymous_leaf
+	      (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast])))
+    | None -> 
 	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast]))
+	  (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast]))
 
 let add_externs pri pat tacast local dbnames = 
   List.iter (add_extern pri pat tacast local) dbnames
@@ -450,7 +526,7 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, UpdateDB (List.map (make_trivial env sigma) l))))
+	 inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l))))
     dbnames
 
 let forward_intern_tac = 
@@ -464,7 +540,7 @@ let add_hints local dbnames0 h =
   let f = Constrintern.interp_constr sigma env in
   match h with
   | HintsResolve lhints ->	
-      add_resolves env sigma (List.map (fun (pri, x) -> pri, f x) lhints) local dbnames
+      add_resolves env sigma (List.map (fun (pri, b, x) -> pri, b, f x) lhints) local dbnames
   | HintsImmediate lhints ->
       add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
@@ -478,21 +554,35 @@ let add_hints local dbnames0 h =
             (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
              str "to an evaluable reference.")
         in
-	  if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+	  Dumpglob.add_glob (loc_of_reference r) gr;
 	 (gr,r') in
       add_unfolds (List.map f lhints) local dbnames
+ | HintsTransparency (lhints, b) ->
+      let f r =
+	let gr = Syntax_def.global_with_alias r in
+        let r' = match gr with
+         | ConstRef c -> EvalConstRef c
+         | VarRef c -> EvalVarRef c
+         | _ -> 
+           errorlabstrm "evalref_of_ref"
+            (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
+             str "to an evaluable reference.")
+        in
+	  Dumpglob.add_glob (loc_of_reference r) gr;
+	  r' in
+      add_transparency (List.map f lhints) b local dbnames
   | HintsConstructors lqid ->
       let add_one qid =
         let env = Global.env() and sigma = Evd.empty in
         let isp = inductive_of_reference qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
         let lcons = list_tabulate
-          (fun i -> None, mkConstruct (isp,i+1)) (Array.length consnames) in
+          (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in
         add_resolves env sigma lcons local dbnames in
       List.iter add_one lqid
   | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in
-      let tacexp = !forward_intern_tac (fst pat) tacexp in
+      let pat =	Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in
+      let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
       add_externs pri pat tacexp local dbnames
   | HintsDestruct(na,pri,loc,pat,code) ->
       if dbnames0<>[] then
@@ -503,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)
@@ -514,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 
@@ -538,19 +628,16 @@ 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)
-      | [] -> assert false 
-    in
+    let (hdc,args) = head_constr_bound cl in
     let hd = head_of_constr_reference hdc in
     let dbs = Hintdbmap.to_list !searchtable in
     let valid_dbs = 
@@ -568,14 +655,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 () = 
@@ -591,9 +678,15 @@ let print_hint_db db =
 	   str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ()));
   Hint_db.iter 
     (fun head hintlist ->
-       msg (hov 0 
-	      (str "For " ++ pr_global head ++ str " -> " ++
-		 fmt_hint_list hintlist)))
+      match head with
+      | Some head ->
+	  msg (hov 0 
+		  (str "For " ++ pr_global head ++ str " -> " ++
+		      pr_hint_list hintlist))
+      | None ->
+	  msg (hov 0 
+		  (str "For any goal -> " ++
+		      pr_hint_list hintlist)))
     db
 
 let print_hint_db_by_name dbname =
@@ -618,7 +711,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) *)
@@ -633,25 +729,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 [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,false) None) lems in
-    Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty 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
@@ -671,10 +775,13 @@ let forward_interp_tactic =
 let set_extern_interp f = forward_interp_tactic := f
 
 let conclPattern concl pat tac gl =
-  let constr_bindings =
-    try matches pat concl
-    with PatternMatchingFailure -> error "conclPattern" in
-  !forward_interp_tactic constr_bindings tac gl
+  let constr_bindings = 
+    match pat with 
+    | None -> []
+    | Some pat ->
+	try matches pat concl
+	with PatternMatchingFailure -> error "conclPattern" in
+    !forward_interp_tactic constr_bindings tac gl
 
 (**************************************************************************)
 (*                           The Trivial tactic                           *)
@@ -684,6 +791,10 @@ let conclPattern concl pat tac gl =
 (* 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 flags_of_state st =
+  {auto_unif_flags with 
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+
 let rec trivial_fail_db mod_delta db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
@@ -697,29 +808,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 (Option.get 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
@@ -727,46 +821,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 -> 
-	  let st = {flags with modulo_delta = Hint_db.transparent_state db} in
-	    List.map (fun x -> (st,x)) (Hint_db.map_all hdc db))
+	  if Hint_db.use_dn db then 
+	    let flags = flags_of_state (Hint_db.transparent_state db) in
+	      List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	  else
+	    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 -> 
-	let (ids, csts as st) = Hint_db.transparent_state db in
-	let st, 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)
+	if Hint_db.use_dn db then 
+	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	    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 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 -> (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 (Option.get 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)
+    let hdconstr,_ = head_constr_bound cl in
+    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 -> 
     []
 
@@ -804,70 +903,82 @@ 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)
+    let hdconstr,_ = head_constr_bound cl in
+    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_empty_term c gls = 
-  let typc = pf_type_of gls c in 
-  let (hd,_) = decompose_app typc in 
-  if Hipattern.is_empty_type hd then 
-    simplest_case c gls 
+let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
+  try
+    let ccl = applist (head_constr typc) in
+    match Hipattern.match_with_conjunction ccl with
+    | Some (_,args) ->
+	tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+    | None ->
+	kont2 gl
+  with UserError _ -> kont2 gl
+
+let decomp_empty_term (id,_,typc) gl = 
+  if Hipattern.is_empty_type typc then 
+    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,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
 
@@ -883,8 +994,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
 
@@ -896,8 +1006,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
@@ -922,14 +1031,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)
 
@@ -952,7 +1062,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) =
   let ents = 
     map_succeed
       (fun f -> f (mkVar id,ty)) 
-      [make_exact_entry None; make_apply_entry env sigma (true,false) None]
+      [make_exact_entry None; make_apply_entry env sigma (true,true,false) None]
   in 
   ents
 
@@ -988,25 +1098,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 =