Fix splitting evars tactics and stop dropping evar constraints when

building a new goal evar defs.
Allow customization of the reduction function applied to subtac
obligations.


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

7 files changed, 60 insertions, 33 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index a10ef1cb66..f1bdd64092 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -149,7 +149,7 @@ let move_after (id, ev, deps as obl) l =
 	  if Intset.is_empty restdeps' then
 	    obl' :: obl :: tl
 	  else obl' :: aux restdeps' tl
-    | [] -> assert false
+    | [] -> [obl]
   in aux (Intset.remove id deps) l
     
 let sort_dependencies evl =
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 9619aa4226..e0ba212c53 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -21,8 +21,8 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
-let reduce =
-  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+let reduce c =
+  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty c
 
 exception NoObligations of identifier option
 
@@ -61,6 +61,7 @@ type program_info = {
   prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
+  prg_reduce : constr -> constr;
   prg_hook : Tacexpr.declaration_hook;
 }
 
@@ -248,7 +249,7 @@ let declare_mutual_definition l =
 	let subs, typ = (subst_body true x) in
 	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
 	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
-	  reduce term, reduce typ, x.prg_implicits) l)
+	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixkind = Option.get first.prg_fixkind in
@@ -278,8 +279,8 @@ let declare_mutual_definition l =
       List.iter progmap_remove l; kn
       
 let declare_obligation prg obl body =
-  let body = reduce body in
-  let ty = reduce obl.obl_type in
+  let body = prg.prg_reduce body in
+  let ty = prg.prg_reduce obl.obl_type in
   match obl.obl_status with
   | Expand -> { obl with obl_body = Some body }
   | Define opaque ->
@@ -299,9 +300,7 @@ let declare_obligation prg obl body =
 	print_message (Subtac_utils.definition_message obl.obl_name);
 	{ obl with obl_body = Some (mkConst constant) }
 
-let red = Reductionops.nf_betaiota Evd.empty
-
-let init_prog_info n b t deps fixkind notations obls impls kind hook =
+let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -315,13 +314,13 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = red t; obl_status = o;
+	      obl_location = l; obl_type = reduce t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
-    { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
+    { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
-      prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
+      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; }
 
 let get_prog name =
   let prg_infos = !from_prg in
@@ -557,9 +556,10 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n term t [] None [] obls implicits kind hook in
+  let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Flags.if_verbose ppnl (str ".");
@@ -574,12 +574,14 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) 
+    ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in
-	  ProgMap.add n prg acc)
+	let prg = init_prog_info n (Some b) t deps (Some fixkind) 
+	  notations obls imps kind reduce hook 
+	in ProgMap.add n prg acc)
       !from_prg l
   in
     from_prg := upd;
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index c1e8d31c0e..aed5b58b7a 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -27,6 +27,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
   ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
+  ?reduce:(Term.constr -> Term.constr) ->
   ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -40,6 +41,7 @@ val add_mutual_definitions :
       (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
+  ?reduce:(Term.constr -> Term.constr) ->
   ?hook:Tacexpr.declaration_hook ->
   notations ->
   fixpoint_kind -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 013270a6a7..8654ca9479 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -677,9 +677,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env evdref lvar c).utj_val 
     in
     if resolve_classes then (
-      evdref :=
-        Typeclasses.resolve_typeclasses ~onlyargs:false
-	  ~split:true ~fail:fail_evar env !evdref);
+      evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	~split:true ~fail:fail_evar env !evdref);
     evdref := consider_remaining_unif_problems env !evdref;
     let c = if expand_evar then nf_evar !evdref c' else c' in
       if fail_evar then check_evars env Evd.empty !evdref c;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6463168985..5275d04c7c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -70,7 +70,7 @@ let evar_filter evi =
     { evi with 
       evar_hyps = Environ.val_of_named_context hyps';
       evar_filter = List.map (fun _ -> true) hyps' }
-      
+
 let evars_to_goals p evm =
   let goals, evm' =
     Evd.fold
@@ -86,6 +86,7 @@ let evars_to_goals p evm =
     if goals = [] then None
     else
       let goals = List.rev goals in
+      let evm' = evars_reset_evd evm' evm in
 	Some (goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
@@ -332,7 +333,14 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
   { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
 
 let solve_tac (x : 'a tac) : 'a tac =
-  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> if gls = [] then sk res fk else fk ()) fk gls }
+  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> 
+    if gls = [] then sk res fk else fk ()) fk gls }
+
+let solve_unif_tac : atac =
+  { skft = fun sk fk {it = gl; sigma = s} -> 
+    try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in
+	  normevars_tac.skft sk fk ({it=gl; sigma=s'})
+    with _ -> fk () }
 
 let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s} ->
@@ -457,7 +465,6 @@ let then_tac (first : atac) (second : atac) : atac =
 let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
   t.skft (fun x _ -> Some x) (fun _ -> None) gl
 
-
 type run_list_res = (auto_result * run_list_res fk) option
 
 let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
@@ -492,7 +499,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
       let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
 	match get_result res with
 	| None -> raise Not_found
-	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
+	| Some (evm', fk) -> Some (evars_reset_evd evm' evm, fk)
 	    
 let eauto_tac hints = 
   fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
@@ -552,16 +559,31 @@ let rec merge_deps deps = function
       else hd :: merge_deps deps tl
 
 let evars_of_evi evi =
-  Intset.union (Evarutil.evars_of_term evi.evar_concl)
-    (match evi.evar_body with
-    | Evar_defined b -> Evarutil.evars_of_term b
-    | Evar_empty -> Intset.empty)
+  Intset.union (evars_of_term evi.evar_concl)
+    (Intset.union
+	(match evi.evar_body with
+	| Evar_empty -> Intset.empty
+	| Evar_defined b -> evars_of_term b)
+	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
+
+let deps_of_constraints cstrs deps =
+  List.fold_right (fun (_, _, x, y) deps -> 
+    let evs = Intset.union (evars_of_term x) (evars_of_term y) in
+      merge_deps evs deps)
+    cstrs deps
+      
+let evar_dependencies evm =
+  Evd.fold 
+    (fun ev evi acc ->
+      merge_deps (Intset.union (Intset.singleton ev) 
+		     (evars_of_evi evi)) acc)
+    evm []
 
 let split_evars evm =
-  Evd.fold (fun ev evi acc ->
-    let deps = Intset.union (Intset.singleton ev) (evars_of_evi evi) in
-      merge_deps deps acc)
-    evm []
+  let _, cstrs = extract_all_conv_pbs evm in
+  let evmdeps = evar_dependencies evm in
+  let deps = deps_of_constraints cstrs evmdeps in
+    List.sort Intset.compare deps
 
 let select_evars evs evm =
   Evd.fold (fun ev evi acc ->
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 9c23be6f0b..a5d1f0d375 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -17,6 +17,8 @@ open Environ
 open Explore
 (*i*)
 
+val hintbases : hint_db_name list option Pcoq.Gram.Entry.e
+val wit_hintbases : hint_db_name list option typed_abstract_argument_type
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
 val rawwit_auto_using : constr_expr list raw_abstract_argument_type
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fdd05b870f..32de48cd7b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -532,7 +532,7 @@ let explain_unsatisfiable_constraints env evd constr =
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
-	pr_constraints true env evm
+	pr_constraints true env undef
   | Some (ev, k) ->
       explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
 	if List.length (Evd.to_list undef) > 1 then