aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
2009-08-04- Add more precise error localisation when one of the application failsherbelin
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-08-02Fixed a typo in "info" for tactic "right".herbelin
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
2009-07-08Simplify addition of hints to a hint_db. Rebuild the dnet associatedmsozeau
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
2009-06-28Raise an error and not an anomaly if a rewrite is attempted on amsozeau
2009-06-22Correct treatment of dependent products in signatures: create the evarsmsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-16Reimplementation of leibniz rewrite to control the instantiation of themsozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-06-11When typing a non-dependent arrow, do not put the (anonymous) variablemsozeau
2009-06-10Use the projections for reflexivity, symmetry and transitivity proofs tomsozeau
2009-06-09Correct handling of the initial existentials from the goal and the onesmsozeau
2009-06-08Do a fixpoint on the result of typeclass search to force themsozeau
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
2009-06-01## Lines starting with '## ' will be removed from the log message.msozeau
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
2009-05-18Minor unification changes:msozeau
2009-05-17- Allowing multiple calls to tactic fix with automatic generation ofherbelin
2009-05-16Minor fixes in typeclasses:msozeau
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-05-05Improvements in typeclasses eauto and generalized rewriting:msozeau
2009-04-28Fixes for bugs in r12110:msozeau
2009-04-27Cleanup old eauto code.msozeau
2009-04-27- Implementation of a new typeclasses eauto procedure based on successmsozeau
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-04-21Rename [Morphism] into [Proper] and [respect] into [proper] to complymsozeau
2009-04-17- Fix handling of clauses in setoid_rewrite to rewrite under bindersmsozeau
2009-04-16Better Requires in Classes. Fix bug #2093: the code does not requiremsozeau
2009-04-16nouvelle version de la tactique groebner proposee par Loic:barras
2009-04-14Rewrite autorewrite to use a dnet indexed by the left-hand sides (ormsozeau
2009-04-14Add a combinator for rewriting given a list of terms and fix themsozeau
2009-04-13Rewrite of setoid_rewrite to modularize it based on proof-producingmsozeau
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-04-10Fix tauto no longer failing after commit 12077; appropriate errorherbelin
2009-04-09Turning tauto into a classical tautology prover as soon as classicalherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 09:55:09 +0000