aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* 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
* meme correction de bug, en moins bourrinGravatar letouzey2004-03-23
* PolyList -> ListGravatar letouzey2004-03-22
* correction d'un bug faisant inliner minus, mult, ...Gravatar letouzey2004-03-22
* petit rajeunissement du test d'extractionGravatar letouzey2004-03-20
* preparation pour release (suite)Gravatar barras2004-03-15
* To make that the translation process does not fail on data produced byGravatar bertot2004-03-15
* oopsGravatar corbinea2004-03-15
* minor changesGravatar corbinea2004-03-14
* congruence now handles disequalitiesGravatar corbinea2004-03-14
* Mise en place temporaire d'un afficheur de 'language' pour le traducteurGravatar herbelin2004-03-13
* Ooops ! bug in firstorder fixed (let's hope no one noticed)Gravatar corbinea2004-03-11
* reals: renamed type option into field_rel_optionGravatar marche2004-03-11
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Reparation ROmega V8/Omega ZERO/POS/NEGGravatar mohring2004-03-04
* adaptation V8 version Pierre CregutGravatar mohring2004-03-03
* takes better account of the new possibility to pass a parametric count argumentGravatar bertot2004-03-03
* removes capital letters in two tactic names.Gravatar bertot2004-03-03
* make sure the implicit argument indications are in the right orderGravatar bertot2004-03-03
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* code mortGravatar herbelin2004-03-01
* Ajout IntroPattern comme type d'argument génériqueGravatar herbelin2004-03-01
* Protection d'un 'clear' qui peut etre dependantGravatar herbelin2004-03-01
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
* Not all cases for coercions and locality were handledGravatar bertot2004-02-26
* corrects the treatement of SubClass declarationsGravatar bertot2004-02-23
* makes sure the following examples are well-treated:Gravatar bertot2004-02-19
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 10:48:15 +0000