aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml/xmlcommand.ml
Commit message (Expand)AuthorAge
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Standardisation of function names about structuresGravatar herbelin2005-02-18
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Orthographe!Gravatar herbelin2004-12-03
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* Nouvelle en-têteGravatar herbelin2004-07-16
* * <style>...</style> tag no longer generated for theory filesGravatar sacerdot2004-07-08
* Constants just after a "Let id : t. ... Qed" local variable declaration wereGravatar sacerdot2004-07-05
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* Licence changed from GPL to Lesser GPL.Gravatar sacerdot2004-06-26
* Copyright notice of files in contrib/xml made uniform.Gravatar sacerdot2004-04-07
* Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;Gravatar sacerdot2004-04-07
* Important bug fix: since coqdoc is now quoting XML reserved characters inGravatar sacerdot2004-04-06
* Since coqdoc produces (X)HTML, HTML character entities can be usedGravatar sacerdot2004-04-05
* ** WARNING **Gravatar sacerdot2004-04-04
* LocalFact added as a choice for the "as" attribute of ht:VARIABLE in theGravatar sacerdot2004-04-01
* Big bug fixed: interactive local definitions where handled as constantsGravatar sacerdot2004-04-01
* Output of theory files reimplemented using Buffer.Gravatar sacerdot2004-04-01
* ~keep_sections was now redundant. Got rid of.Gravatar sacerdot2004-04-01
* En mode batch, recuperation via Declare de l'information si un inductive est ...Gravatar herbelin2004-03-31
* *** WARNING: DTD Change ***Gravatar sacerdot2004-03-30
* declare_internal_constant behaved as declare_constant for proofs (e.g.Gravatar sacerdot2004-03-30
* No longer used (and probably no longer working) code removed.Gravatar sacerdot2004-03-30
* Added a <br/> after "Require ...".Gravatar sacerdot2004-03-30
* RenommageGravatar herbelin2004-03-30
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-03-30
* Fabrication de l'uri a partir du path utilisateurGravatar herbelin2004-03-30
* Retrait debogageGravatar herbelin2004-03-29
* Export du type de preuve en cours pour xmlGravatar herbelin2004-03-29
* Debug prints removed.Gravatar sacerdot2004-03-29
* Export RequireGravatar herbelin2004-03-29
* Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversGravatar herbelin2004-03-27
* -dead code removed.Gravatar sacerdot2004-03-27
* Theory file for file A.B.C.v is put in A/B/C.theory.xml.Gravatar sacerdot2004-03-26
* Ajout exportation des 'theory.xml' + diversGravatar herbelin2004-03-26
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
* Dead code removed.Gravatar sacerdot2004-03-25
* Reparation typo de HH dans MAJ de ClaudioGravatar herbelin2004-03-24
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration de la branche mowgliGravatar herbelin2002-11-05
* reparation du make depend et du .dependGravatar letouzey2001-12-19
* Mise en place d'une méthode directe pour indiquer le type des déclarations ...Gravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 09:16:38 +0000