aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml4
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Allow setoid rewrite to rewrite in pattern-matching scrutinees orGravatar msozeau2009-09-09
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Support globality flag properly for "Add Morphism foo : foo_mor" syntax.Gravatar msozeau2009-09-03
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* 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
* Raise an error and not an anomaly if a rewrite is attempted on aGravatar msozeau2009-06-28
* Correct treatment of dependent products in signatures: create the evarsGravatar msozeau2009-06-22
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Use the projections for reflexivity, symmetry and transitivity proofs toGravatar msozeau2009-06-10
* Correct handling of the initial existentials from the goal and the onesGravatar msozeau2009-06-09
* Minor unification changes:Gravatar msozeau2009-05-18
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* - Fix handling of clauses in setoid_rewrite to rewrite under bindersGravatar msozeau2009-04-17
* Better Requires in Classes. Fix bug #2093: the code does not requireGravatar msozeau2009-04-16
* Rewrite autorewrite to use a dnet indexed by the left-hand sides (orGravatar msozeau2009-04-14
* Add a combinator for rewriting given a list of terms and fix theGravatar msozeau2009-04-14
* Rewrite of setoid_rewrite to modularize it based on proof-producingGravatar msozeau2009-04-13
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 00:57:18 +0000