aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Fixes to make Ynot compile with the trunk:Gravatar msozeau2009-03-20
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* - Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideGravatar herbelin2008-12-18
* About "apply in":Gravatar herbelin2008-12-09
* Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bGravatar herbelin2008-11-23
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fix wrong environment bug in test for setoid_rewrite or rewrite.Gravatar msozeau2008-07-28
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* A better test for relations being setoids or not: do leibniz rewrite iffGravatar msozeau2008-07-25
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* Correction petit bug sur révision 11159 (res_pf fait un effet de bordGravatar herbelin2008-06-21
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Bug squashing day !Gravatar msozeau2008-04-17
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* correction de bug dans Function et augmentation de la classe des fonctions su...Gravatar jforest2007-05-17
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Proposition de correction pour le bug #1173 (ou du moins pour unGravatar herbelin2007-04-13
* Changement mineur du comportement de 'rewrite .. in * |-': si leGravatar notin2007-03-30
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Correction bug #1439 (comportement de replace by)Gravatar notin2007-03-13
* Correction typo liée au commit 8779 (levait une anomalie)Gravatar herbelin2007-02-21
* remplacement d'un test d'egalite par un test de convertibilite dans injection...Gravatar jforest2006-12-22
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:34:40 +0000