aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-02-14encodage des typesfilliatr
2007-02-14tactique yicesfilliatr
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2007-02-12Bug mineur dans la generation des principes d'induction pour Functionjforest
2007-02-12Autres passages de Set à Type dans Relations et Wellfoundedherbelin
2007-02-12Fix matching on dependent types, taking a safe stand.msozeau
2007-02-11Correction d'un bug dans la génération des principes d'inductionjforest
2007-02-11Add keywords that were missing, notably for terms.msozeau
2007-02-09Suppresion de la catégorie des inductifs singletons larges dontherbelin
2007-02-09bugfix sufficescorbinea
2007-02-09Retour r9310 en attendant mieuxherbelin
2007-02-09Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...notin
2007-02-09Separate Tactics in subtac.msozeau
2007-02-08Add lif then else for if in bool.msozeau
2007-02-08Fix myinjection tactic, generalize coercion for applicationsmsozeau
2007-02-07Fix mistake naming my Tactics file Tactics :)msozeau
2007-02-07Add tactics for induction on subterms.msozeau
2007-02-07Meilleur anglais (cf 9619)herbelin
2007-02-07Vérification que toutes les evars ont étés instanciées dans les types imp...herbelin
2007-02-07Correction bug #1364 (les variables de section sont repérées parherbelin
2007-02-07Relecture/nettoyage chapitre Gallina; déplacement section Functionherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 08:12:21 +0000