aboutsummaryrefslogtreecommitdiff
path: root/plugins/interface
diff options
context:
space:
mode:
authorherbelin2009-11-26 16:28:17 +0000
committerherbelin2009-11-26 16:28:17 +0000
commit23f26304a9132e09105d6580a1d3caf72053a859 (patch)
treea079aa0c379784220020694ef94b07ebd5b51401 /plugins/interface
parentc84fd703d6d00494e62b0fa5fb609cda67132133 (diff)
Fixing xml theory file export (was not consistent with coqdoc file
naming heuristic). Added a corresponding test. Note: maybe should the generated .v file for exporting the theory be made of a valid ident if ever coqdoc eventually follows coq convention: currently it has name foo.theory.v which is not coqc-compilable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12543 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface')
0 files changed, 0 insertions, 0 deletions