aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
Commit message (Expand)AuthorAge
* nouveau module ZdivGravatar filliatr2002-04-05
* Elimination Elimdep.vGravatar mohring2002-03-27
* ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...Gravatar letouzey2002-01-18
* mise a jourGravatar filliatr2001-12-10
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Deplacement des setoides.Gravatar clrenard2001-09-19
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
* Changement de place et de nom de la tactique Setoid_rewrite.Gravatar clrenard2001-07-10
* Mise a jour des .dependGravatar clrenard2001-06-26
* Ajouts des theories du paradoxe de BerardiGravatar delahaye2001-06-19
* Ajout des entrees puor Setoid_replace.Gravatar clrenard2001-06-12
* Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...Gravatar herbelin2001-05-31
* Ajout de Rseries et Rtrigo_funGravatar mayero2001-04-24
* Ajout Fourier, DiscrR, ...Gravatar mayero2001-04-20
* support option -R pour coqdepGravatar filliatr2001-04-20
* Zarith -> ZArithGravatar filliatr2001-04-19
* Ajout de FieldGravatar delahaye2001-04-19
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* Added two files that are used for the connection with the graphical user-inte...Gravatar bertot2001-04-04
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
* mise a jourGravatar filliatr2000-11-29
* MAJGravatar herbelin2000-11-26
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* MAJGravatar herbelin2000-11-20
* mise a jourGravatar filliatr2000-11-15
* Finalement PolyListSyntax est necessaire (la redondance venait d'une confusio...Gravatar herbelin2000-11-10
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* MAJGravatar herbelin2000-11-05
* Few OCaml files in contrib/xmlGravatar sacerdot2000-11-03
* ntrefiner.ml* removed in module xmlGravatar sacerdot2000-10-26
* xml contribution added to the MakefileGravatar sacerdot2000-10-25
* mise a jour dependancesGravatar filliatr2000-09-18
* portage RefineGravatar filliatr2000-07-20
* portage EAuto et RingGravatar filliatr2000-06-21
* mise a jourGravatar filliatr2000-06-12
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
* portage en ocaml / camlp4 3.00Gravatar filliatr2000-04-28
* TautoGravatar filliatr2000-03-20
* ZArithGravatar filliatr2000-03-18
* bug discharge (work_alist contenanti plein de fois les memes choses)Gravatar filliatr2000-03-18
* compilation theories/ArithGravatar filliatr2000-03-10
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Restructuration diversesGravatar herbelin2000-01-07
* documentationGravatar filliatr1999-12-13