aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:01 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:01 +0000
commit98db1b73f6ab89763ef386a2055528db91e4e152 (patch)
tree1743e12160bef3ace6ea46fa00f5618df65ebecc /library/lib.ml
parente4c505927b0ebe06f87ecc14567431822e8e0b5c (diff)
Remove code concerning the obsolete Set/Unset Undo
Even if they are no-ops now, the commands Set/Unset Undo themselves are kept for compatibility, in particular to avoid error messages or warnings during the initialization of ProofGeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
0 files changed, 0 insertions, 0 deletions