aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libobject.mli
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-15 07:16:48 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-15 07:16:48 +0000
commite4639721323887555d278b963b84b11244871632 (patch)
tree9befc6971b6d255ba22ddee337f7471e218c6273 /library/libobject.mli
parentb49a6d54a0b43b9d15b073a1a2c384714d49987b (diff)
-opt ne remplace plus camlp4 par camlp4o.opt car on ne peut pas
charger de bytecode avec camlp4o.opt (et la compilation échoue sur parsing/pcoq.ml4 dans ce cas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@850 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libobject.mli')
0 files changed, 0 insertions, 0 deletions