aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
2008-07-25A better test for relations being setoids or not: do leibniz rewrite iffmsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-06-21Correction petit bug sur révision 11159 (res_pf fait un effet de bordherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-04-17Bug squashing day !msozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-04Quelques améliorations des intro patterns:herbelin
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-03-01Rework on rich forms of rewriteletouzey
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-17correction de bug dans Function et augmentation de la classe des fonctions su...jforest
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-13Proposition de correction pour le bug #1173 (ou du moins pour unherbelin
2007-03-30Changement mineur du comportement de 'rewrite .. in * |-': si lenotin
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-03-13Correction bug #1439 (comportement de replace by)notin
2007-02-21Correction typo liée au commit 8779 (levait une anomalie)herbelin
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans injection...jforest
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
2006-10-03Changement de comportement du [rewrite ... in H]: Coq échoue si Hnotin
2006-10-03Retour sur la suppression du pf_nf (trop d'exemples utilisent avecherbelin
2006-10-01Une passe sur l'injection et la discrimination...herbelin
2006-09-30Suppression de la comparaison (inutile) des paramètres globaux desherbelin
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-07-05Correcting for bug #1167 jforest
2006-06-12Updating documentation of replace and correcting a typo in error message of r...jforest
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-05-20"subst." works now even when it exists an hypothesis have the form "x=x" in t...jforest
2006-05-02Extension syntaxique de rewrite in: au lieu de pouvoir faire letouzey
2006-05-02Changement de comportement de rewrite: face a une egalité setoid, onletouzey
2006-04-02Correction bug 1119 (inversion marche a moitie dans Type)herbelin
2006-03-21+ destruct now works as induction on multiple arguments : jforest
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
2005-12-30Nettoyage coqlibherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-09-08Réparation bug #1004; nettoyageherbelin