aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hints.ml')
-rw-r--r--tactics/hints.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d1343f296..89ecc6c0b 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 =