aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-04-07Move setoid_rewrite to its own module and do some clean up inmsozeau
2009-04-05Display the content of the list instead of "<list>" when an idtacherbelin
2009-03-31Fix auto so that Extern tactics associated to no patterns can apply tomsozeau
2009-03-28Fix useless redeclaration of a tactic name when UpdateTac is replayed.msozeau
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
2009-03-22Compromise wrt introduction-names compatibility issue after additionherbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Fixes to make Ynot compile with the trunk:msozeau
2009-03-19coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...barras
2009-03-17Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 16:18:28 +0000