aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Applied greenrd's patch to fix bug 2255 (injection failed toGravatar herbelin2010-03-27
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Completion of r12580 (better rendering of dependent rewrite and inversion).Gravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Improved the rendering of "dependent rewrite" and hence of "inversion"Gravatar herbelin2009-12-12
* Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameGravatar herbelin2009-12-03
* Addendum to revision 12501.Gravatar herbelin2009-11-12
* Backtracking on the use of automatically generated schemes forGravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Stop trying to search if the relation is declared as a [RewriteRelation]Gravatar msozeau2009-09-09
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Fixed subst failing when a truly heterogeneous JMeq hyp is in theGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 11:05:28 +0000