aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Nom qualifié pour option -topGravatar herbelin2004-03-28
* Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...Gravatar herbelin2004-03-28
* MAJGravatar herbelin2004-03-28
* Ajout option -top pour changer le nom 'Top' du toplevelGravatar herbelin2004-03-28
* Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...Gravatar herbelin2004-03-28
* Crochets pour exported les sections en xmlGravatar herbelin2004-03-27
* Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversGravatar herbelin2004-03-27
* Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...Gravatar herbelin2004-03-27
* Export compute_arguments_scope pour utilisation local a la construction des i...Gravatar herbelin2004-03-27
* -dead code removed.Gravatar sacerdot2004-03-27
* majGravatar filliatr2004-03-27
* majGravatar filliatr2004-03-27
* Theory file for file A.B.C.v is put in A/B/C.theory.xml.Gravatar sacerdot2004-03-26
* Ajout option raw-comments pour supprimer affichage de <table>Gravatar herbelin2004-03-26
* Ajout option raw-comments pour supprimer affichage de <table>; typosGravatar herbelin2004-03-26
* MAJ mot-clesGravatar herbelin2004-03-26
* Bug <BR>; ajout option raw_comment pas d'affichage de <table>; MAJ mot-clesGravatar herbelin2004-03-26
* Ajout exportation des 'theory.xml' + diversGravatar herbelin2004-03-26
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
* Ajout entree pour exporter les commentaires en mode -xmlGravatar herbelin2004-03-26
* Memorisation du type de variable (Hyp or Var)Gravatar herbelin2004-03-26
* *** empty log message ***Gravatar barras2004-03-26
* majGravatar filliatr2004-03-26
* Code mortGravatar herbelin2004-03-25
* 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
* ProofTree2Xml is no longer directly used by Xmlcommand.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
* majGravatar filliatr2004-03-25
* majGravatar filliatr2004-03-25
* MAJ commentairesGravatar herbelin2004-03-24
* *** empty log message ***Gravatar barras2004-03-24
* 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
* bug de PP des fix (coqbugs #574)Gravatar barras2004-03-24
* *** empty log message ***Gravatar barras2004-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
* code mortGravatar herbelin2004-03-24
* nouvelle commande Set Extraction Flag: reglage fins des optimsGravatar letouzey2004-03-24
* majGravatar filliatr2004-03-24