aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorglondu2011-10-20 05:47:47 +0000
committerglondu2011-10-20 05:47:47 +0000
commit1ffb37b4651dcc7a2b1d59285e07ea9e2a3febe5 (patch)
treeb9cc664926542fa6203b50a889b35bcb77d2a584 /plugins
parent6b1c2cd00381381a187588ab9f59b68bb5b01850 (diff)
More descriptive error messages in checker
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14576 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions