aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix matching on dependent types, taking a safe stand.Gravatar msozeau2007-02-12
* Correction d'un bug dans la génération des principes d'inductionGravatar jforest2007-02-11
* Add keywords that were missing, notably for terms.Gravatar msozeau2007-02-11
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
* bugfix sufficesGravatar corbinea2007-02-09
* Retour r9310 en attendant mieuxGravatar herbelin2007-02-09
* Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...Gravatar notin2007-02-09
* Separate Tactics in subtac.Gravatar msozeau2007-02-09
* Add lif then else for if in bool.Gravatar msozeau2007-02-08
* Fix myinjection tactic, generalize coercion for applicationsGravatar msozeau2007-02-08
* Fix mistake naming my Tactics file Tactics :)Gravatar msozeau2007-02-07
* Add tactics for induction on subterms.Gravatar msozeau2007-02-07
* Meilleur anglais (cf 9619)Gravatar herbelin2007-02-07
* Vérification que toutes les evars ont étés instanciées dans les types imp...Gravatar herbelin2007-02-07
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
* Suppression RefMan-cas.tex inutiliséGravatar herbelin2007-02-07
* Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueGravatar herbelin2007-02-07
* Various subtac fixes. Add inequalities in pattern matching branches when need...Gravatar msozeau2007-02-07
* Field rewrites only with polynomialGravatar thery2007-02-07
* doc de ring/field + option infinite -> completenessGravatar barras2007-02-07
* Report de la révision 9599 de la v8.1 dans le trunkGravatar notin2007-02-06
* Passage de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-06
* doc for fieldGravatar thery2007-02-06
* complement du commit 9591Gravatar bgregoir2007-02-05
* changement dans ring specification du sign, divisionGravatar bgregoir2007-02-05
* Work on ineqs generation.Gravatar msozeau2007-02-03
* Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterGravatar herbelin2007-02-02
* field: introduction de Get_goalGravatar bgregoir2007-02-02
* ring: introduction de Get_goalGravatar bgregoir2007-02-02
* Now 1/x * x simplifies to 1Gravatar thery2007-02-02
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
* Suppression de code mortGravatar notin2007-02-01
* Report 9545 de 8.1 vers trunkGravatar herbelin2007-02-01
* Petite relecture partie ringGravatar herbelin2007-02-01
* Report de la révision 9577 dans le trunkGravatar notin2007-02-01
* Abbreviation of order notation.Gravatar msozeau2007-02-01
* report de r9574: doc de fieldGravatar barras2007-01-31
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
* MAJ ringGravatar herbelin2007-01-31
* Correction typo eq_rec_eq (cf bug #1339)Gravatar herbelin2007-01-31
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
* Fix typo.Gravatar msozeau2007-01-31
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
* suite du commit 9557 Gravatar soubiran2007-01-30
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
* constr_of_pat bug with nested patterns.Gravatar msozeau2007-01-30
* bugfix for suffices (support for open head)Gravatar corbinea2007-01-29
* Various fixes in subtac, update some test cases.Gravatar msozeau2007-01-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 10:29:20 +0000