aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/fix.v
diff options
context:
space:
mode:
authorGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-25 15:55:16 +0000
committerGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-25 15:55:16 +0000
commita4bd836942106154703e10805405e8b4e6eb11ee (patch)
tree704e5ab788a7d9d27b85828a89c43705741d6e79 /test-suite/success/fix.v
parent166714d89845f7e2f894fcd0fd92ae16961ca9eb (diff)
correction bug 1839
is line, and those below, will be ignored-- M kernel/mod_subst.mli M kernel/mod_typing.ml M kernel/mod_subst.ml M kernel/subtyping.ml M kernel/modops.ml M library/declaremods.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/fix.v')
0 files changed, 0 insertions, 0 deletions