Turn evars created by a tactic application into a subgoal immediately in

typeclass resolution. Makes the backtracking heuristic correct again and
avoids "late" backtracking on an unsolvable existential. Compilation
time is back to normal.


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

1 files changed, 19 insertions, 6 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f89528487..23d92429e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -342,17 +342,30 @@ let hints_tac hints =
 	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
 	    aux (succ i) tl)
 	  in
-	  let gls' = list_map_i (fun j g -> 
+	  let sgls = evars_to_goals (fun evm ev evi ->
+	    if Typeclasses.is_resolvable evi && 
+	      (not info.only_classes || Typeclasses.is_class_evar evm evi) then
+	      Typeclasses.mark_unresolvable evi, true
+	    else evi, false) s
+	  in
+	  let nbgls, newgls, s' =
+	    let gls' = List.map (fun g -> (None, g)) gls in
+	    match sgls with
+	    | None -> List.length gls', gls', s
+	    | Some (evgls, s') ->
+		(List.length gls', gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s')
+	  in
+	  let gls' = list_map_i (fun j (evar, g) -> 
 	    let info = 
 	      { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
-		is_evar = None;
+		is_evar = evar;
 		hints = 
 		  if b && g.evar_hyps <> gl.evar_hyps 
 		  then make_autogoal_hints info.only_classes
-		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s}
+		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
 		  else info.hints }
-	    in g, info) 1 gls in
-	  let glsv = {it = gls'; sigma = s}, (fun _ -> v) in
+	    in g, info) 1 newgls in
+	  let glsv = {it = gls'; sigma = s'}, (fun _ pfl -> v (list_firstn nbgls pfl)) in
 	    sk glsv fk
       | [] -> fk ()
     in aux 1 tacs }
@@ -378,7 +391,7 @@ let occur_evars evars c =
 let dependent only_classes evd oev concl =
   let concl_evars = Intset.union (evars_of_term concl)
     (Option.cata Intset.singleton Intset.empty oev)
-  in not (Intset.is_empty concl_evars)
+  in not (Intset.is_empty concl_evars) 
 
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : (autogoal list * validation) list) fk = function