aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-04-13Correction confusion entre la dependance en les termes filtrees dans l'annota...herbelin
2004-04-12majfilliatr
2004-04-11majfilliatr
2004-04-09majfilliatr
2004-04-08majfilliatr
2004-04-08Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...herbelin
2004-04-08Incoherence bytecamlc et camlc si echec a trouver ocamlc.opt avec option -opt...herbelin
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
2004-04-07majfilliatr
2004-04-07majfilliatr
2004-04-07Old file. The new version of this script is no longer distributed withsacerdot
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
2004-04-07preparation a la release 8.0barras
2004-04-07*** empty log message ***barras
2004-04-07bug #606: mis un message d'erreur plus clairbarras
2004-04-07CoRN CProp detection improved: products of "sort" CProp are now recognizedsacerdot
2004-04-07Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;sacerdot
2004-04-07A few changes backtracked:sacerdot
2004-04-06majfilliatr
2004-04-061. In -html mode the generated files are well-formed XML filessacerdot
2004-04-06Fake dependent products in inductive definition types are no longer replacedsacerdot
2004-04-06Premier jet annonce finaleherbelin
2004-04-06Important bug fix: since coqdoc is now quoting XML reserved characters insacerdot
2004-04-06MAJ V8.0 finaleherbelin
2004-04-06sumbool et sumor affich avec 'if' si possibleherbelin
2004-04-06warning dialog when save failsmarche
2004-04-06Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)herbelin
2004-04-06echappement de <, > et & en HTMLfilliatr
2004-04-05majfilliatr
2004-04-05Déclaration des record au chargement (ce n'est pas une question de visibilit...herbelin
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-02majfilliatr
2004-04-01majfilliatr
2004-04-01majfilliatr
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-31majfilliatr
2004-03-31majfilliatr
2004-03-31Morphismes déclarés comme Lemma pas comme Definitionherbelin
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ...herbelin
2004-03-31Export de l'information si un inductive est un record ou non (pour xml)herbelin
2004-03-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
2004-03-30majfilliatr
2004-03-30*** WARNING: DTD Change ***sacerdot
2004-03-30The XML exportation hook for require is now active for:sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 04:07:16 +0000