Generalize fix for auto from PMP to eauto and typeclasses eauto.

4 files changed, 46 insertions, 39 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 617c491c35..a6b53d76cc 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,16 +72,14 @@ let auto_flags_of_state st =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
+let connect_hint_clenv poly (c, _, ctx) clenv gl =
   (** [clenv] has been generated by a hint-making function, so the only relevant
       data in its evarmap is the set of metas. The [evar_reset_evd] function
       below just replaces the metas of sigma by those coming from the clenv. *)
   let sigma = Proofview.Goal.sigma gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (** Still, we need to update the universes *)
-  let (_, _, ctx) = c in
-  let clenv =
+  let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
@@ -91,11 +89,15 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
       (** FIXME: We're being inefficient here because we substitute the whole
           evar map instead of just its metas, which are the only ones
           mentioning the old universes. *)
-      Clenv.map_clenv map clenv
+      Clenv.map_clenv map clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }
-  in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
+  in clenv, c
+		     
+let unify_resolve poly flags ((c : raw_hint), clenv) =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
   Clenvtac.clenv_refine false clenv
   end
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 6e2acf7f56..cae180ce76 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -25,6 +25,9 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
+val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
+			 [ `NF ] Proofview.Goal.t -> clausenv * constr
+						
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36b60385d8..f3a4863444 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -154,33 +154,31 @@ let e_give_exact flags poly (c,clenv) gl =
     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
 let unify_e_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv'
 
 let unify_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic 
-    (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv'
 
-let clenv_of_prods poly nprods (c, clenv) gls =
+let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some clenv
   else
-    let ty = pf_unsafe_type_of gls c in
+    let ty = Tacmach.New.pf_unsafe_type_of gl c in
     let diff = nb_prod ty - nprods in
       if Pervasives.(>=) diff 0 then
         (* Was Some clenv... *)
-	Some (mk_clenv_from_n gls (Some diff) (c,ty))
+	Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
       else None
 
-let with_prods nprods poly (c, clenv) f gls =
-  match clenv_of_prods poly nprods (c, clenv) gls with
-  | None -> tclFAIL 0 (str"Not enough premisses") gls
-  | Some clenv' -> f (c, clenv') gls
+let with_prods nprods poly (c, clenv) f =
+  Proofview.Goal.nf_enter (fun gl ->
+  match clenv_of_prods poly nprods (c, clenv) gl with
+  | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+  | Some clenv' -> f (c, clenv') gl)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
@@ -224,12 +222,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
       let tac = function
-      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
-      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+      | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
       | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
       | Res_pf_THEN_trivial_fail (term,cl) ->
-          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+         Proofview.V82.tactic (tclTHEN
+				 (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
+				 (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
       | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
       | Extern tacast -> conclPattern concl p tacast
       in
@@ -847,4 +846,5 @@ let autoapply c i gl =
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  unify_e_resolve false flags (c,ce) gl
+  let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in
+  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 09c5fa873f..ca430ec111 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -116,15 +116,17 @@ open Unification
 (***************************************************************************)
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-
-let unify_e_resolve poly flags (c,clenv) gls =
-  let (c, _, _) = c in
-  let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv 
-  else clenv, Univ.empty_level_subst in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-    tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-      (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
+			  
+let unify_e_resolve poly flags (c,clenv) =
+  Proofview.Goal.nf_enter begin
+      fun gl ->
+      let clenv', c = connect_hint_clenv poly c clenv gl in
+      Proofview.V82.tactic
+	(fun gls ->
+	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
+	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+    end
 
 let hintmap_of hdc concl =
   match hdc with
@@ -166,10 +168,10 @@ and e_my_find_search db_list local_db hdc concl =
       (b,
         let tac = function
         | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
-        | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+        | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
         | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
         | Res_pf_THEN_trivial_fail (term,cl) ->
-          Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
+          Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl)))
             (e_trivial_fail_db db_list local_db))
         | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
         | Extern tacast -> conclPattern concl p tacast