aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml/xmlcommand.mli
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
DTDs licence is still GPL. This should create no problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ↵herbelin
un record; restructuration en consequence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5623 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations ↵herbelin
utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout exportation des 'theory.xml' + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5576 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25ProofTree2Xml is no longer directly used by Xmlcommand.sacerdot
On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained design is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5563 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5548 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration de la branche mowgliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Report des modifs de Claudioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-07COPYRIGHT file added; some comments changedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1080 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Many improvements. Xml contrib retached to the V7.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@994 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03URI problem addressed, but not resolved yetsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@796 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25xml contribution created.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:20:05 +0000