Merge branch 'v8.5'

6 files changed, 57 insertions, 43 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9ca6162a21..dc4ac55b23 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 c30957a673..83b1202b72 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -167,33 +167,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 *)
 
@@ -237,12 +235,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
@@ -902,4 +901,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 1a84161e40..d0fd4b0780 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -124,15 +124,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
@@ -176,10 +178,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) -> e_exact poly st (c,cl)
         | Res_pf_THEN_trivial_fail (term,cl) ->
-          Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_e_resolve poly st (term,cl)))
+          Tacticals.New.tclTHEN (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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c6d74525fe..740a165f8d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1130,7 +1130,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
-	| None -> anomaly (Pp.str "Not enough components to build the dependent tuple")
+	| None ->
+            (* This at least happens if what has been detected as a
+               dependency is not one; use an evasive error message;
+               even if the problem is upwards: unification should be
+               tried in the first place in make_iterated_tuple instead
+               of approximatively computing the free rels; then
+               unsolved evars would mean not binding rel *)
+	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
     !evdref, Evarutil.nf_evar !evdref scf
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ec6f041336..895064951d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -45,8 +45,8 @@ open Proofview.Notations
 
 let safe_msgnl s =
   Proofview.NonLogical.catch
-    (Proofview.NonLogical.print (s++fnl()))
-    (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
+    (Proofview.NonLogical.print_debug (s++fnl()))
+    (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
 
 type value = tlevel generic_argument
 
@@ -1151,7 +1151,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         interp_message ist s >>= fun msg ->
         return (hov 0 msg , hov 0 msg)
       in
-      let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in
+      let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in
       let log (msg,_) = Proofview.Trace.log (fun () -> msg) in
       let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in
       Ftactic.run msgnl begin fun msgnl ->