From d8e87360b6413d9eb02c2c47441c8f48b816eac3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Oct 2016 19:06:10 +0200
Subject: Using "simple apply" and "simple eapply" in the trace of auto.

This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
---
 tactics/hints.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d1343f296e..89ecc6c0b2 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1297,11 +1297,11 @@ let make_db_list dbnames =
 let pr_hint_elt (c, _, _) = pr_constr c
 
 let pr_hint h = match h.obj with
-  | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
-  | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
+  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
   | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
   | Res_pf_THEN_trivial_fail (c, _) ->
-      (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
+      (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
-- 
cgit v1.2.3