aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-04-24adding binary files that are needed for the graphical user-interface pcoqbertot
2001-04-24Removing a debug message for the search command.bertot
2001-04-23Ajout de syntaxe pour Ltacdelahaye
2001-04-23Ajout Realsmayero
2001-04-23Ajouts Realsmayero
2001-04-23(One more) Minor layout adjustments for Library doccoq
2001-04-23forme codefilliatr
2001-04-23Minor layout adjustments for Library doccoq
2001-04-23mise a jourletouzey
2001-04-23realisation des realsletouzey
2001-04-23un warning pas beau supprimméfilliatr
2001-04-23Gros nain avec de Bruijn...letouzey
2001-04-23diversfilliatr
2001-04-23nettoyagefilliatr
2001-04-23expansion des constr pursfilliatr
2001-04-23reduction des let in dans whd_programsfilliatr
2001-04-23version 7.0 finalefilliatr
2001-04-23Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.letouzey
2001-04-23Remaniement Makefile de test. make reals possibleletouzey
2001-04-23patch Claudio pour coq_makefilefilliatr
2001-04-20test Fourier, DiscrRmayero
2001-04-20Ajout tactics Realsmayero
2001-04-20Ajout Fouriermayero
2001-04-20Ajout Fourier, DiscrR, ...mayero
2001-04-20Library doc adjustments (until page 140)coq
2001-04-20optimizations extractionfilliatr
2001-04-20the file vernacrc, that is necessary to the graphical user-interface pcoqbertot
2001-04-20Mise a la norme lexicalemohring
2001-04-20Decomposition de Casesmohring
2001-04-20Erreurs de Casesmohring
2001-04-20Retire commenatires obsoletesmohring
2001-04-20*** empty log message ***mohring
2001-04-20un typage sûr pour Goal et Checkfilliatr
2001-04-20Hints.... added next to Hint....coq
2001-04-20Ajout d'erreurs sur le Case avec branche redondantemohring
2001-04-20Tests pour Field avec les nombres reelsdelahaye
2001-04-20Ajout de la ligne d'etat pour CVSdelahaye
2001-04-20Petit menagedelahaye
2001-04-20Ajout des entetesdelahaye
2001-04-20support option -R pour coqdepfilliatr
2001-04-20nettoyagefilliatr
2001-04-19Add a treatement of elaborate Intros tactics, CONJPATTERN and family.bertot
2001-04-19Cd est silencieux si -silentfilliatr
2001-04-19typofilliatr
2001-04-19scripts; extraction False_recfilliatr
2001-04-19blindage False_recfilliatr
2001-04-19cofix; axiomes; eta-expansions pour variables de types mal generalisees (en c...filliatr
2001-04-19Zarith -> ZArithfilliatr
2001-04-19ajout du cas win32courant
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring