aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
...
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:22:12 +0000