aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2001-04-19Ajout de Bool/BoolEq.vmohring
2001-04-19BoolEq.v, une egalite generique a valeur dans boolmohring
2001-04-19ZArith --> Zarithmohring
2001-04-19synchonization des tables d'extractionfilliatr
2001-04-19remplace Zarith par ZArithmohring
2001-04-19Changement Zarith ZArithmohring
2001-04-19remplace Zarith par ZArithmohring
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19modifs des scripts de test autofilliatr
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19*** empty log message ***mohring
2001-04-19Remplacement Euclid_def Euclid_proof par Euclidmohring
2001-04-19deplacement de l'optimisation inductif singletonletouzey
2001-04-19script de bench automatique pour extractionletouzey
2001-04-19Making sure there will be no warnings at compile time.bertot
2001-04-19-boot n'implique plus -batchfilliatr
2001-04-19*** empty log message ***courant
2001-04-19Changement syntax pour Rinvmayero
2001-04-19*** empty log message ***mayero
2001-04-19Ajout de Fielddelahaye
2001-04-19Fonction lookup enleveedelahaye