diff options
| author | Hugo Herbelin | 2014-11-22 15:20:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-22 19:23:33 +0100 |
| commit | c3bb115fa765278bc3bcb3beb8c74b0fb8b35d98 (patch) | |
| tree | d4c6a1f78ec210d8b0100144251ca236ff1902cd | |
| parent | b3320b0f942a9f86d5bd1c00876f8816e5c94446 (diff) | |
Specific printer of Evar.Set.t for ocamldebug + more information in
a UserError to ease debugging.
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | tactics/tacticMatching.ml | 2 |
2 files changed, 2 insertions, 1 deletions
@@ -9,6 +9,7 @@ install_printer Top_printers.ppidset install_printer Top_printers.ppevar install_printer Top_printers.ppevarsubst install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppexistentialset install_printer Top_printers.ppintset install_printer Top_printers.pplab install_printer Top_printers.ppdir 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 |