aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hints.ml')
-rw-r--r--tactics/hints.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 48a7b3f75..70e62eaba 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -912,7 +912,7 @@ let make_resolve_hyp env sigma decl =
(c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
with
| Failure _ -> []
- | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
+ | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.")
(* REM : in most cases hintname = id *)