aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
AgeCommit message (Collapse)Author
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-04-07Old file. The new version of this script is no longer distributed withsacerdot
Coq (the latest verion can be retrieved from the HELM and MoWGLI pages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5658 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
- copyright notice inserted in every DTD git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5657 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
generates not well-formed XML files). An hook is left in xmlcommand.ml to register a pretty-printer function once a fixed implementation is provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07CoRN CProp detection improved: products of "sort" CProp are now recognizedsacerdot
(they used to be exported as products of sort Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5652 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;sacerdot
^ ... ^ special verbatim code also backtracked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5651 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06Fake dependent products in inductive definition types are no longer replacedsacerdot
with non dependent products. The main motivation is that inductive definition parameters often occurs as non-dependent products in the product types, but the binder names are still necessary to render the definition in the usual Coq way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5646 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06Important bug fix: since coqdoc is now quoting XML reserved characters insacerdot
HTML tags (i.e. # ... #), strong verbatim tags must be now used (i.e. ^ ... ^). WARNING: it requires the fortcoming commit on coqdoc to work properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5644 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-05Since coqdoc produces (X)HTML, HTML character entities can be usedsacerdot
in .v files. The exportation module produces generic XML ==> the character entities that were verbatim copied were never declared and the generated files were not well-formed XML files. Fixed by adding to the internal subset of the DTD an inclusion to the three files were the (X)HTML entities are defined. Due to technical reasons (HELM Getter URL rewriting), the chosen URL refers to the HELM web site. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5636 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-04** WARNING **sacerdot
DTD Change. ht:DEFINITION/Definition differentiated into ht:DEFINITION/Definition and ht:DEFINITION/InteractiveDefinition because of an explicit request of Iris Loeb. HELM/MoWGLI DTD and Stylesheet changed accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5634 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01LocalFact added as a choice for the "as" attribute of ht:VARIABLE in thesacerdot
DTD. Used for local proofs (e.g. "Let x : True. auto. Qed."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5630 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01Big bug fixed: interactive local definitions where handled as constantssacerdot
and not as variables. Partially fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5629 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01Output of theory files reimplemented using Buffer.sacerdot
This avoids stdout cluttering in interactive mode. Whenever verbose is set to true, all the strings sent to the Buffer are also printed on stdoud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5628 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01~keep_sections was now redundant. Got rid of.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5627 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-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
The idea is: 1. constructors are always declare by hand by the user ==> binders always have a meaning. 2. the binders are fundamental for record fields, even if the dependent product is really non-dependent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30*** WARNING: DTD Change ***sacerdot
@name of ht:SECTION renamed in @uri Its semantics has not changed (it is the base URI of relative URIs defined inside the section). HELM/MoWGLI stylesheets updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5619 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30declare_internal_constant behaved as declare_constant for proofs (e.g.sacerdot
*_subproof) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5617 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30No longer used (and probably no longer working) code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5614 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Added a <br/> after "Require ...".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5613 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30syntax error: dandling insacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5612 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5611 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-302 choix incorrectsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 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-30Fabrication de l'uri a partir du path utilisateurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5608 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Retrait debogageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5605 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Export du type de preuve en cours pour xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5604 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Debug prints removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5600 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Export Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5599 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5587 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27-dead code removed.sacerdot
-latin1 is now the default in place of utf8 (since several .v files are latin1). Authomatic detection should be implemented. -fixed bug due to the wrong location of html files searched git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5584 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Theory file for file A.B.C.v is put in A/B/C.theory.xml.sacerdot
It was put in file A/B/C/C.theory.xml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5581 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-25The DTD that describes the CIC (with Explicit Named Substitutions) format.sacerdot
A very brief description of the DTD is in the README file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5569 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Fix and Cofix blocks with mutually defined functions having the samesacerdot
name generated XML code with ambiguous names. Example: Inductive t : Set := k : t' -> t with t' : Set := k' : t -> t'. Scheme t_csc := Induction for t Sort Prop with t'_csc := Induction for t' Sort Prop. Print XML t_csc. used to show two functions both named F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5568 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Updated.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5565 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-25No longer used.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5561 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Dead code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5560 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Comment removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5559 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24MAJ Claudio pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5554 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24Reparation typo de HH dans MAJ de Claudioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5553 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24MAJ Claudio pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5552 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24Utilisation du printer approprie a la version de syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5551 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
2004-03-24Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ↵herbelin
version non ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5547 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 05:37:14 +0000