From c3bb115fa765278bc3bcb3beb8c74b0fb8b35d98 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 22 Nov 2014 15:20:04 +0100 Subject: Specific printer of Evar.Set.t for ocamldebug + more information in a UserError to ease debugging. --- tactics/tacticMatching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index fa1b7f1586..c662fad0be 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 -- cgit v1.2.3