aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/predicate.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-18 16:57:32 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-18 16:57:32 +0000
commit4a3c8ae008d0159e4626497e94fd820489a2cf54 (patch)
treef35ecdef638b4361bc48b403f1fe5059a0cd7de2 /lib/predicate.ml
parentddc9c1bd8e1eaae186468f093e467d8f2e1091cd (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 'lib/predicate.ml')
0 files changed, 0 insertions, 0 deletions