Merge branch 'v8.5'

3 files changed, 30 insertions, 18 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index eaaef45fce..789bcd1bdd 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -133,6 +133,14 @@ let unify_e_resolve poly flags (c,clenv) gls =
     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 hintmap_of hdc concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none db
+  | Some hdc ->
+    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
+    else (fun db -> Hint_db.map_auto hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
 let e_exact poly flags (c,clenv) =
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
@@ -155,16 +163,11 @@ let rec e_trivial_fail_db db_list local_db =
   end
 
 and e_my_find_search db_list local_db hdc concl =
+  let hint_of_db = hintmap_of hdc concl in
   let hintl =
-    if occur_existential concl then
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
-   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
-    else
-      List.map_append (fun db ->
-	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -185,17 +188,14 @@ and e_my_find_search db_list local_db hdc concl =
   List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
-  try
-    priority
-      (e_my_find_search db_list local_db
-	 (decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try priority (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd
-    (e_my_find_search db_list local_db
-	(decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try List.map snd (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let find_first_goal gls =
   try first_goal gls with UserError _ -> assert false
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3b497faab5..af541b8b9e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-	   strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto.");
+	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
@@ -1973,6 +1973,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 trivial\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1984,6 +1990,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
   | TacAuto (debug,n,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_auto\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 auto\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 013270b0bd..ccf4795d68 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -882,7 +882,7 @@ let msg_quantified_hypothesis = function
   | NamedHyp id ->
       str "quantified hypothesis named " ++ pr_id id
   | AnonHyp n ->
-      int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+      pr_nth n ++
       str " non dependent hypothesis"
 
 let depth_of_quantified_hypothesis red h gl =