aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2004-04-05Since coqdoc produces (X)HTML, HTML character entities can be usedsacerdot
2004-04-05correction rapide du bug PR\#592letouzey
2004-04-04** WARNING **sacerdot
2004-04-01LocalFact added as a choice for the "as" attribute of ht:VARIABLE in thesacerdot
2004-04-01Big bug fixed: interactive local definitions where handled as constantssacerdot
2004-04-01Output of theory files reimplemented using Buffer.sacerdot
2004-04-01~keep_sections was now redundant. Got rid of.sacerdot
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ...herbelin
2004-03-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
2004-03-30*** WARNING: DTD Change ***sacerdot
2004-03-30declare_internal_constant behaved as declare_constant for proofs (e.g.sacerdot
2004-03-30No longer used (and probably no longer working) code removed.sacerdot
2004-03-30Added a <br/> after "Require ...".sacerdot
2004-03-30syntax error: dandling insacerdot
2004-03-30Renommageherbelin
2004-03-302 choix incorrectsherbelin
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations uti...herbelin
2004-03-30Fabrication de l'uri a partir du path utilisateurherbelin
2004-03-29Retrait debogageherbelin
2004-03-29Export du type de preuve en cours pour xmlherbelin
2004-03-29Debug prints removed.sacerdot
2004-03-29Export Requireherbelin
2004-03-27Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversherbelin
2004-03-27-dead code removed.sacerdot
2004-03-26Theory file for file A.B.C.v is put in A/B/C.theory.xml.sacerdot
2004-03-26Ajout exportation des 'theory.xml' + diversherbelin
2004-03-25The DTD that describes the CIC (with Explicit Named Substitutions) format.sacerdot
2004-03-25Fix and Cofix blocks with mutually defined functions having the samesacerdot
2004-03-25me = andouilleletouzey
2004-03-25Selon les optims, le let-in peut avoir maintenant des argsletouzey
2004-03-25Updated.sacerdot
2004-03-25ProofTree2Xml is no longer directly used by Xmlcommand.sacerdot
2004-03-25No longer used.sacerdot
2004-03-25Dead code removed.sacerdot
2004-03-25Comment removed.sacerdot
2004-03-24MAJ Claudio pour v8herbelin
2004-03-24Reparation typo de HH dans MAJ de Claudioherbelin
2004-03-24MAJ Claudio pour v8herbelin
2004-03-24Utilisation du printer approprie a la version de syntaxeherbelin
2004-03-24Nettoyageherbelin
2004-03-24Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ver...herbelin
2004-03-24nouvelle commande Set Extraction Flag: reglage fins des optimsletouzey
2004-03-23meme correction de bug, en moins bourrinletouzey
2004-03-22PolyList -> Listletouzey
2004-03-22correction d'un bug faisant inliner minus, mult, ...letouzey
2004-03-20petit rajeunissement du test d'extractionletouzey
2004-03-15preparation pour release (suite)barras
2004-03-15To make that the translation process does not fail on data produced bybertot
2004-03-15oopscorbinea
2004-03-14minor changescorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:46:37 +0000