diff options
| author | puech | 2011-07-29 14:24:15 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:24:15 +0000 |
| commit | cde1b816313b9d5b060c5325797d6ba493c68708 (patch) | |
| tree | f776a2d5c7f26808711a726d52260e016c7a80bb /plugins/xml/xmlcommand.ml | |
| parent | e471d37d1c93966d85b7005b796921ead6c18cfd (diff) | |
Term: slight reorganization of the file
- removed duplicate constructors
- moved code around for more clarity
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions