| Age | Commit message (Expand) | Author |
|---|
| 2007-02-24 | Opacity parameterization for obligations working. | msozeau |
| 2007-02-23 | Debug wellfounded defs, work on cleaning obls envs | msozeau |
| 2007-02-22 | Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #... | notin |
| 2007-02-19 | Correct coq depend, add eq_rect elimination tactic to SubtacTactics | msozeau |
| 2007-02-19 | Various little subtac fixes, add some useful tactics. | msozeau |
| 2007-02-16 | Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils. | msozeau |
| 2007-02-16 | lift params appropriately, do not need to coerce to tycon | msozeau |
| 2007-02-16 | Update implementation for dependent types. Works just as well as before for s... | msozeau |
| 2007-02-14 | encodage des types | filliatr |
| 2007-02-14 | tactique yices | filliatr |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-02-12 | Bug mineur dans la generation des principes d'induction pour Function | jforest |
| 2007-02-12 | Fix matching on dependent types, taking a safe stand. | msozeau |
| 2007-02-11 | Correction d'un bug dans la génération des principes d'induction | jforest |
| 2007-02-09 | Retour r9310 en attendant mieux | herbelin |
| 2007-02-09 | Separate Tactics in subtac. | msozeau |
| 2007-02-08 | Add lif then else for if in bool. | msozeau |
| 2007-02-08 | Fix myinjection tactic, generalize coercion for applications | msozeau |
| 2007-02-07 | Fix mistake naming my Tactics file Tactics :) | msozeau |
| 2007-02-07 | Add tactics for induction on subterms. | msozeau |
| 2007-02-07 | Meilleur anglais (cf 9619) | herbelin |
| 2007-02-07 | Various subtac fixes. Add inequalities in pattern matching branches when need... | msozeau |
| 2007-02-07 | doc de ring/field + option infinite -> completeness | barras |
| 2007-02-05 | changement dans ring specification du sign, division | bgregoir |
| 2007-02-03 | Work on ineqs generation. | msozeau |
| 2007-02-02 | Factorisation de la règle Constr.binder dans g_subtac.ml pour éviter | herbelin |
| 2007-02-02 | field: introduction de Get_goal | bgregoir |
| 2007-02-02 | ring: introduction de Get_goal | bgregoir |
| 2007-02-02 | Now 1/x * x simplifies to 1 | thery |
| 2007-02-01 | Abbreviation of order notation. | msozeau |
| 2007-01-30 | constr_of_pat bug with nested patterns. | msozeau |
| 2007-01-29 | Various fixes in subtac, update some test cases. | msozeau |
| 2007-01-29 | Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes. | msozeau |
| 2007-01-28 | "suffices" implemented + syntax cleanup | corbinea |
| 2007-01-26 | Contounement d'un probleme avec la VM dans Function | jforest |
| 2007-01-24 | Update some tests and fix section bug. | msozeau |
| 2007-01-24 | changement de la fonction norm_subst | bgregoir |
| 2007-01-23 | ring : Correction du bug PR#1306 | bgregoir |
| 2007-01-22 | Correction du bug #1315: | notin |
| 2007-01-22 | Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent | herbelin |
| 2007-01-19 | Protection contre les warnings 'unused variable' de ocaml 3.09 | herbelin |
| 2007-01-15 | Various subtac fixes. | msozeau |
| 2007-01-12 | Suite au mail de Lionel a propos du Makefile: | letouzey |
| 2007-01-12 | un saut de ligne ... | letouzey |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2007-01-10 | Nouvelle approche pour le discharge modulaire | herbelin |
| 2007-01-08 | Subtac fixes, support for reasoning on wf defs. | msozeau |
| 2007-01-05 | suite de la reparation du bug 1239: apres les inds, les records et vars de types | letouzey |
| 2007-01-02 | Rework subtac pattern matching equalities generation. | msozeau |
| 2006-12-28 | Remplacement de la définition de Pind et Prec par une définition | herbelin |
