| Commit message (Expand) | Author | Age |
* | About "apply in": | herbelin | 2008-12-09 |
* | Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b | herbelin | 2008-11-23 |
* | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin | 2008-11-22 |
* | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau | 2008-11-05 |
* | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin | 2008-10-26 |
* | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
* | Add a type argument to letin_tac instead of using casts and recomputing | msozeau | 2008-09-12 |
* | Évolutions diverses et variées. | herbelin | 2008-08-04 |
* | Fix wrong environment bug in test for setoid_rewrite or rewrite. | msozeau | 2008-07-28 |
* | Even better test for choosing rewrite or setoid_rewrite. | msozeau | 2008-07-26 |
* | A better test for relations being setoids or not: do leibniz rewrite iff | msozeau | 2008-07-25 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | Rename obligations_tactic to obligation_tactic and fix bugs #1893. | msozeau | 2008-06-22 |
* | Correction petit bug sur révision 11159 (res_pf fait un effet de bord | herbelin | 2008-06-21 |
* | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin | 2008-06-21 |
* | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
* | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
* | Bug squashing day ! | msozeau | 2008-04-17 |
* | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau | 2008-04-12 |
* | Quelques améliorations des intro patterns: | herbelin | 2008-04-04 |
* | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
* | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
* | Rework on rich forms of rewrite | letouzey | 2008-03-01 |
* | Added the automatic generation of the boolean equality if possible and the | vsiles | 2007-10-05 |
* | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
* | Uniformisation politique de nommage evd/isevars (evd si evar_defs, | herbelin | 2007-09-06 |
* | Adding a syntax for "n-ary" rewrite: | letouzey | 2007-07-06 |
* | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin | 2007-05-29 |
* | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
* | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest | 2007-05-17 |
* | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
* | Proposition de correction pour le bug #1173 (ou du moins pour un | herbelin | 2007-04-13 |
* | Changement mineur du comportement de 'rewrite .. in * |-': si le | notin | 2007-03-30 |
* | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin | 2007-03-15 |
* | Correction bug #1439 (comportement de replace by) | notin | 2007-03-13 |
* | Correction typo liée au commit 8779 (levait une anomalie) | herbelin | 2007-02-21 |
* | remplacement d'un test d'egalite par un test de convertibilite dans injection... | jforest | 2006-12-22 |
* | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey | 2006-10-05 |
* | Changement de comportement du [rewrite ... in H]: Coq échoue si H | notin | 2006-10-03 |
* | Retour sur la suppression du pf_nf (trop d'exemples utilisent avec | herbelin | 2006-10-03 |
* | Une passe sur l'injection et la discrimination... | herbelin | 2006-10-01 |
* | Suppression de la comparaison (inutile) des paramètres globaux des | herbelin | 2006-09-30 |
* | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest | 2006-08-22 |
* | Correcting for bug #1167 | jforest | 2006-07-05 |
* | Updating documentation of replace and correcting a typo in error message of r... | jforest | 2006-06-12 |
* | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
* | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
* | "subst." works now even when it exists an hypothesis have the form "x=x" in t... | jforest | 2006-05-20 |
* | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey | 2006-05-02 |
* | Changement de comportement de rewrite: face a une egalité setoid, on | letouzey | 2006-05-02 |