aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Copyright notice of files in contrib/xml made uniform.Gravatar sacerdot2004-04-07
* Old file. The new version of this script is no longer distributed withGravatar sacerdot2004-04-07
* - theoryobject.dtd is the DTD for .theory filesGravatar sacerdot2004-04-07
* Loic code to pretty-print the generated proof-tree debranched (since itGravatar sacerdot2004-04-07
* CoRN CProp detection improved: products of "sort" CProp are now recognizedGravatar sacerdot2004-04-07
* Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;Gravatar sacerdot2004-04-07
* Fake dependent products in inductive definition types are no longer replacedGravatar sacerdot2004-04-06
* 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
* correction rapide du bug PR\#592Gravatar letouzey2004-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
* Fake dependent types in constructors of inductive types are now preserved.Gravatar sacerdot2004-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
* syntax error: dandling inGravatar sacerdot2004-03-30
* RenommageGravatar herbelin2004-03-30
* 2 choix incorrectsGravatar 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
* The DTD that describes the CIC (with Explicit Named Substitutions) format.Gravatar sacerdot2004-03-25
* Fix and Cofix blocks with mutually defined functions having the sameGravatar sacerdot2004-03-25
* me = andouilleGravatar letouzey2004-03-25
* Selon les optims, le let-in peut avoir maintenant des argsGravatar letouzey2004-03-25
* Updated.Gravatar sacerdot2004-03-25
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
* No longer used.Gravatar sacerdot2004-03-25
* Dead code removed.Gravatar sacerdot2004-03-25
* Comment removed.Gravatar sacerdot2004-03-25
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
* Reparation typo de HH dans MAJ de ClaudioGravatar herbelin2004-03-24
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
* Utilisation du printer approprie a la version de syntaxeGravatar herbelin2004-03-24
* NettoyageGravatar herbelin2004-03-24
* Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ver...Gravatar herbelin2004-03-24
* nouvelle commande Set Extraction Flag: reglage fins des optimsGravatar letouzey2004-03-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 19:01:33 +0000