diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 16:57:32 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 16:57:32 +0000 |
| commit | 4a3c8ae008d0159e4626497e94fd820489a2cf54 (patch) | |
| tree | f35ecdef638b4361bc48b403f1fe5059a0cd7de2 /checker/check.mllib | |
| parent | ddc9c1bd8e1eaae186468f093e467d8f2e1091cd (diff) | |
Added exception enrichment. Now one can define additional arbitrary
information worn by exceptions. The implementation is quite hackish
but it should work nonetheless.
Basically, it adds an additional cell to exceptions arguments, in
which you can put whatever you want. By typing invariants, you may
not reach this cell by normal means, so it should be safe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.mllib')
| -rw-r--r-- | checker/check.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 2d56e163b..e468f1292 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,4 +1,5 @@ Coq_config +Exninfo Backtrace Int Pp_control |