aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-02-07Suppression RefMan-cas.tex inutiliséherbelin
2007-02-07Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueherbelin
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when need...msozeau
2007-02-07Field rewrites only with polynomialthery
2007-02-07doc de ring/field + option infinite -> completenessbarras
2007-02-06Report de la révision 9599 de la v8.1 dans le trunknotin
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
2007-02-06doc for fieldthery
2007-02-05complement du commit 9591bgregoir
2007-02-05changement dans ring specification du sign, divisionbgregoir
2007-02-03Work on ineqs generation.msozeau
2007-02-02Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterherbelin
2007-02-02field: introduction de Get_goalbgregoir
2007-02-02ring: introduction de Get_goalbgregoir
2007-02-02Now 1/x * x simplifies to 1thery
2007-02-01Report de révision 9583 de la v8.1 dans le trunknotin
2007-02-01Suppression de code mortnotin
2007-02-01Report 9545 de 8.1 vers trunkherbelin
2007-02-01Petite relecture partie ringherbelin
2007-02-01Report de la révision 9577 dans le trunknotin
2007-02-01Abbreviation of order notation.msozeau
2007-01-31report de r9574: doc de fieldbarras
2007-01-31Correction d'un bug dans check_and_clear_in_constr + simplification denotin
2007-01-31MAJ ringherbelin
2007-01-31Correction typo eq_rec_eq (cf bug #1339)herbelin
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
2007-01-31Fix typo.msozeau
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
2007-01-30Nouvelle implantation de clear_hypsnotin
2007-01-30suite du commit 9557 soubiran
2007-01-30Petite correction sur un message d'erreur renvoyé au sous typage.soubiran
2007-01-30constr_of_pat bug with nested patterns.msozeau
2007-01-29bugfix for suffices (support for open head)corbinea
2007-01-29Various fixes in subtac, update some test cases.msozeau
2007-01-29finalized sufficescorbinea
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
2007-01-28"suffices" implemented + syntax cleanupcorbinea
2007-01-28Pas de solution à court terme pour ce problème de complexitéherbelin
2007-01-26Explication du intros until nnotin
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
2007-01-26correction d'un bug d'efficacite dans le printerjforest
2007-01-25decl mode: anonymous factscorbinea
2007-01-25Redondance erronée dans les testsherbelin
2007-01-24doc de ringbgregoir
2007-01-24modifications des messages d'erreurs renvoyés lors de la comparaison soubiran
2007-01-24Update some tests and fix section bug.msozeau
2007-01-24changement de la fonction norm_substbgregoir
2007-01-24Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentherbelin
2007-01-24Correction bug #1333 (test non récursivité des dépendances en d'autresherbelin
2007-01-23Updated Makefile to include ConstructiveEpsilon.vemakarov
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 11:26:02 +0000