aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Turning tauto into a classical tautology prover as soon as classicalGravatar herbelin2009-04-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
* Display the content of the list instead of "<list>" when an idtacGravatar herbelin2009-04-05
* Fix auto so that Extern tactics associated to no patterns can apply toGravatar msozeau2009-03-31
* Fix useless redeclaration of a tactic name when UpdateTac is replayed.Gravatar msozeau2009-03-28
* Backport from v8.2 branch of 11986 (interpretation of quantifiedGravatar herbelin2009-03-22
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Fixes to make Ynot compile with the trunk:Gravatar msozeau2009-03-20
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* - gros commit sur ring et field: passage des arguments simplifieGravatar barras2009-03-17
* 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
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:31:03 +0000