aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2001-04-19Metas dans les Unfold'sdelahaye
2001-04-19Essais dans Ltacdelahaye
2001-04-19make sure the binaries needed for the graphical interface will also bebertot
2001-04-18Correcting a problem of s that appears behind a Let when there arebertot
2001-04-18there was a wrong order in the previous version. One was trying tobertot
2001-04-18Make sure the binaries needed for pcoq are compiled by default.bertot
2001-04-18Erreur Makefile JMeqmohring
2001-04-18Changing the commands to switch to textual explanation of proofs.bertot
2001-04-18Adding files for the production of textual explanations as used in pcoq.bertot
2001-04-16*** empty log message ***courant
2001-04-15MAJherbelin
2001-04-15Mise en pageherbelin
2001-04-15to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...herbelin
2001-04-15Suppression de mk_constr qui ne respectait pas l'invariant des applications (...herbelin
2001-04-15Bug affichage d'implicites pour les vars lieesherbelin
2001-04-15Bug affichage ordre des variables d'un patternherbelin
2001-04-14Reparation du bug de Trydelahaye
2001-04-14Non parenthesage des applications de tactiquesdelahaye
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
2001-04-13Reparation de l'affichage des THEN'sdelahaye
2001-04-13eliminiation des singletons du genre sig + diversletouzey
2001-04-13ajout de testsmohring
2001-04-13MAJherbelin
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-04-12nouvelle gestion des variables de type MLletouzey
2001-04-12Mis un message d'erreur explicite pour l'echec de Elim en casmohring
2001-04-12Ajout de l'egalite de John Majormohring
2001-04-11coqwebfilliatr
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-04-11réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...filliatr
2001-04-11Bug rapporte par Randy en Mars 2000herbelin
2001-04-10bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_appletouzey
2001-04-10-I contrib/extraction pour compiler Extraction.vfilliatr
2001-04-10portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegafilliatr
2001-04-10Modified searchPattern. Before this correction, constructors were overlooked,bertot
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-10bug lift dans IsRel de extract_type. Axiomes dans extract_typeletouzey
2001-04-10Mise a jour de la config pour distribmohring
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:05:54 +0000