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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index fa6d9324c..0b6ec899e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,5 +1,6 @@ Coq_config +Exninfo Backtrace Int Pp_control |