aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_prim.ml4
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-07 14:01:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-07 14:01:59 +0000
commit2be0079f2ed4b67eae474341a10b9f60dcf83c4f (patch)
tree97e03cde10cff22588e9019477d16febb93fc75e /parsing/g_prim.ml4
parent670a61a7ca4c55a5e06a79a73989a52bf0cb2273 (diff)
Extraction Library Foo creates Foo.ml, not foo.ml
And similarly for Haskell: we do not force capitalized/uncapitalized filenames anymore, but we rather follow the name of the .v file (with new extensions of course). Ok, this is an incompatible change, but it is really convenient, some people where actually already doing some hacks to have this behavior (cf. Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_prim.ml4')
0 files changed, 0 insertions, 0 deletions