aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-03-05 11:59:35 +0100
committerGuillaume Melquiond2015-03-05 11:59:46 +0100
commit141620b00d4d6e39d0ee86b69b3987582472840f (patch)
tree2a63f15c6e907d007a4f77db9854dbcdaaf20909 /kernel/nativelambda.ml
parent9b4849d9d2271f91a6e32675d792a68951cbc2b6 (diff)
Preprend Fail to all the expected failures in the documentation.
This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions