aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-06-26*** empty log message ***mohring
2002-06-26*** empty log message ***mohring
2002-06-26Resolution de bug (du a Auto; remplacement par lt_O_Sn)mayero
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
2002-06-25Integration de Rcomplet et Alembert_compldesmettr
2002-06-25*** empty log message ***desmettr
2002-06-21Suppression de l'axiome d'extensionnalitedesmettr
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-06-20Nouvelle version avec INR + Amelioration de Sup0.mayero
2002-06-20*** empty log message ***desmettr
2002-06-20majfilliatr
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19Reparation de ring pour les setoidesclrenard
2002-06-19ProgWf -> Zwffilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-19Coercion de la syntaxe des motifs non atomiquesherbelin
2002-06-18coq_makefile utilise maintenant coqdocfilliatr
2002-06-17Suppression de fct_eqdesmettr
2002-06-17Prise en compte de exp, cosh et sinhdesmettr
2002-06-17Modifications relatives a l'ajout de Rtrigo_defdesmettr
2002-06-17Definitions de exp, cos et sindesmettr
2002-06-17*** empty log message ***desmettr
2002-06-14*** empty log message ***herbelin
2002-06-14Commentairesherbelin
2002-06-14*** empty log message ***herbelin
2002-06-13Bug non vérification non redondance par Cutherbelin
2002-06-13Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...herbelin
2002-06-13Test de l'interprétation des fermetures de Match Context (2ème)herbelin
2002-06-13Ajout map_inductive_type et map_ind_familyherbelin
2002-06-13Test de l'interprétation des fermetures de Match Contextherbelin
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
2002-06-13Petits beug d'affichages.gregoire
2002-06-11Tests pour la tactique Regdesmettr
2002-06-11*** empty log message ***desmettr
2002-06-11*** empty log message ***desmettr
2002-06-11Ranalysis.vdesmettr
2002-06-07L'ordre supérieur avait quelque peu été oublié dans l'unification...herbelin
2002-06-07extraction vers schemeletouzey
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
2002-06-07Ajout de FNL ou utilisation de msgnlherbelin
2002-06-07Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputherbelin
2002-06-07I added a comment on the tactic compute_POS.bertot
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
2002-06-06Ajout exemple JCF conflit variable interne, variable de sectionherbelin
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après e...herbelin
2002-06-06Des exemples sérieuxherbelin
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs de...herbelin
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 19:07:37 +0000