diff options
| author | Hugo Herbelin | 2016-10-14 19:06:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-14 20:00:28 +0200 |
| commit | d8e87360b6413d9eb02c2c47441c8f48b816eac3 (patch) | |
| tree | 3bfd16c875d116cc520088ea6c74d2646d0c829d | |
| parent | db18609c06b73ac168ad06a0c2073188587f5814 (diff) | |
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).
| -rw-r--r-- | tactics/hints.ml | 6 |
1 files 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 = |