aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tacticMatching.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index fa1b7f158..c662fad0b 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -102,7 +102,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
(merged, Id.Map.merge merge lcm lm)
let matching_error =
- Errors.UserError ("" , Pp.str "No matching clauses for match.")
+ Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
(** A functor is introduced to share the environment and the
evar_map. They do not change and it would be a pity to introduce