aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* 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
* Fixed a typo in "info" for tactic "right".Gravatar herbelin2009-08-02
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Simplify addition of hints to a hint_db. Rebuild the dnet associatedGravatar msozeau2009-07-08
* 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
* 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
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar 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
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2009-06-01
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Minor unification changes:Gravatar msozeau2009-05-18
* - Allowing multiple calls to tactic fix with automatic generation ofGravatar herbelin2009-05-17
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
* Fixes for bugs in r12110:Gravatar msozeau2009-04-28
* Cleanup old eauto code.Gravatar msozeau2009-04-27
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* 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
* nouvelle version de la tactique groebner proposee par Loic:Gravatar barras2009-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
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Fix tauto no longer failing after commit 12077; appropriate errorGravatar herbelin2009-04-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 21:38:54 +0000