aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Important bug fix: since coqdoc is now quoting XML reserved characters inGravatar sacerdot2004-04-06
* MAJ V8.0 finaleGravatar herbelin2004-04-06
* sumbool et sumor affich avec 'if' si possibleGravatar herbelin2004-04-06
* warning dialog when save failsGravatar marche2004-04-06
* Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)Gravatar herbelin2004-04-06
* echappement de <, > et & en HTMLGravatar filliatr2004-04-06
* majGravatar filliatr2004-04-05
* Déclaration des record au chargement (ce n'est pas une question de visibilit...Gravatar herbelin2004-04-05
* 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
* majGravatar filliatr2004-04-02
* majGravatar filliatr2004-04-01
* majGravatar filliatr2004-04-01
* 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
* majGravatar filliatr2004-03-31
* majGravatar filliatr2004-03-31
* Morphismes déclarés comme Lemma pas comme DefinitionGravatar herbelin2004-03-31
* En mode batch, recuperation via Declare de l'information si un inductive est ...Gravatar herbelin2004-03-31
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* Fake dependent types in constructors of inductive types are now preserved.Gravatar sacerdot2004-03-31
* majGravatar filliatr2004-03-30
* *** WARNING: DTD Change ***Gravatar sacerdot2004-03-30
* The XML exportation hook for require is now active for:Gravatar sacerdot2004-03-30
* declare_internal_constant behaved as declare_constant for proofs (e.g.Gravatar sacerdot2004-03-30
* Heuristique pour traduire if-then-else quand le re-typage echoueGravatar herbelin2004-03-30
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-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
* majGravatar filliatr2004-03-29
* majGravatar filliatr2004-03-29
* Retrait debogageGravatar herbelin2004-03-29
* Export du type de preuve en cours pour xmlGravatar herbelin2004-03-29
* tools/coq_vo2xml removed since no longer in use.Gravatar sacerdot2004-03-29
* "xml" target removed from generated makefiles (since it was no longer used)Gravatar sacerdot2004-03-29
* MAJGravatar kirchner2004-03-29
* Debug prints removed.Gravatar sacerdot2004-03-29
* Export RequireGravatar herbelin2004-03-29
* Crocret xml pour RequireGravatar herbelin2004-03-29
* CommentairesGravatar herbelin2004-03-29
* TypoGravatar herbelin2004-03-29
* majGravatar filliatr2004-03-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 10:38:33 +0000