| Age | Commit message (Expand) | Author |
|---|
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-05-17 | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-04-29 | Orthographe en passant | herbelin |
| 2007-04-29 | Ajout possibilité d'options à trois mots. | herbelin |
| 2007-04-28 | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-25 | New keyword "Inline" for Parameters and Axioms for automatic | soubiran |
| 2007-04-17 | Correct implementation of undo in obligations handling code, correct some bug... | msozeau |
| 2007-04-16 | Export de simplest_eapply, utilisé dans la contrib interface | notin |
| 2007-04-05 | Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func... | jforest |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2007-03-28 | Support for implicit formal argument types in Program ; parse types in type s... | msozeau |
| 2007-03-26 | Make multiple patterns work again with Program while simplifying the code. | msozeau |
| 2007-03-20 | Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a... | msozeau |
| 2007-03-20 | traces Ergo | filliatr |
| 2007-03-19 | Forgot to update to new cast | msozeau |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-03-16 | r11153@tannat: jforest | 2007-03-16 10:25:55 +0100 | jforest |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2007-03-15 | Add destruct_call variant where naming of introduced hypotheses is possible. ... | msozeau |
| 2007-03-14 | Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ... | msozeau |
| 2007-03-13 | Solve obligation handling bug of trying to solve automatically at Next Obliga... | msozeau |
| 2007-03-11 | correction du bug 1432 | jforest |
| 2007-03-11 | Remove bugguy notations | msozeau |
| 2007-03-08 | Create a program_scope in subtac Utils | msozeau |
| 2007-02-28 | The right tactics for definitions using measures. | msozeau |
| 2007-02-27 | Fix wf bug from F. Besson and work on ineqs generation. | msozeau |
| 2007-02-24 | Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar) | herbelin |
| 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 |
