| Commit message (Expand) | Author | Age |
|---|
| * | Various minor improvements of comments in mli for ocamldoc |  letouzey | 2010-04-29 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation |  pboutill | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Fixed bug #2999 (destruct was not refreshing universes of what it generalized *) |  herbelin | 2010-04-20 |
| * | Fixed some printing bugs. | herbelin | 2010-04-18 |
| * | Solved a few problems of auto by bypassing the call to apply. | herbelin | 2010-04-17 |
| * | Use nice "unfold" instead of ugly "change" to display calls to unfold hints | herbelin | 2010-04-17 |
| * | Util: remove list_split_at which is a clone of list_chop | letouzey | 2010-04-16 |
| * | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin | 2010-04-14 |
| * | Improving compatibility between 8.2 and 8.3 | herbelin | 2010-04-05 |
| * | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
| * | Applied greenrd's patch to fix bug 2255 (injection failed to | herbelin | 2010-03-27 |
| * | Fix splitting evars tactics and stop dropping evar constraints when |  msozeau | 2010-03-15 |
| * | fixed confusion between number of cstr arguments and number of pattern variab... |  barras | 2010-03-12 |
| * | Fix lifting of constraints in generalized rewriting tactic. | msozeau | 2010-03-07 |
| * | Fixes in rewrite and a Elimination/Case to Scheme: | msozeau | 2010-03-06 |
| * | Improvements in generalized rewriting: | msozeau | 2010-03-05 |
| * | Fix [autounfold] to accept general [in] clauses. | msozeau | 2010-03-05 |
| * | Add a generic tactic option builder. Use it in firstorder to set the | msozeau | 2010-03-05 |
| * | Fix [Existing Class] impl and add documentation. Fix computation of the | msozeau | 2010-02-10 |
| * | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau | 2010-01-30 |
| * | Support for generalized rewriting under dependent binders, using the | msozeau | 2010-01-26 |
| * | Quick fix for references to section variables unbound in the current | msozeau | 2010-01-26 |
| * | New version of 12650 that was broken (supporting again records when | herbelin | 2010-01-12 |
| * | Added module sharing support for typeclasses and hints (pri_auto_tactic). |  soubiran | 2010-01-12 |
| * | revert commit 12650 for the moment, since it breaks MSetAVL | letouzey | 2010-01-12 |
| * | Temporary fix to compensate the loss of descent on dependent | herbelin | 2010-01-12 |
| * | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin | 2009-12-30 |
| * | Improving descend_in_conjunctions (using a combinators instead of a tactic) | herbelin | 2009-12-29 |
| * | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin | 2009-12-28 |
| * | Fix "Existing Instance" to handle globality information and "Existing | msozeau | 2009-12-27 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
| * | Moved a bit further the code for pattern interpretation in match goal | herbelin | 2009-12-23 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | Backtrack on making exact hints for lemmas starting with products | msozeau | 2009-12-19 |
| * | adding an option functional_induction_rewrite_dependent to make functional in... |  jforest | 2009-12-16 |
| * | Improved strategy for rewriting lemma possibly depending because of evars. | herbelin | 2009-12-14 |
| * | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin | 2009-12-13 |
| * | Completion of r12580 (better rendering of dependent rewrite and inversion). | herbelin | 2009-12-13 |
| * | Revision 12557 continued (better rendering of dependent rewrite) | herbelin | 2009-12-13 |
| * | Updated compatibility for rewriting equality proofs that are dependent | herbelin | 2009-12-12 |
| * | Improved the rendering of "dependent rewrite" and hence of "inversion" | herbelin | 2009-12-12 |
| * | Turn evars created by a tactic application into a subgoal immediately in | msozeau | 2009-12-06 |
| * | Fix anomaly when using typeclass resolution with filtered hyps in evars. | msozeau | 2009-12-06 |
| * | Restored rewriting of JMeq using JMeq_rect and co when the domains are the same | herbelin | 2009-12-03 |
| * | Fix make_exact_entry to allow applying [forall x, P x] hints directly, | msozeau | 2009-12-01 |
| * | Fix bug in typeclass resolution. Better handling of universes in | msozeau | 2009-12-01 |
| * | Fix backtracking heuristic in typeclass resolution. | msozeau | 2009-11-30 |
letouzey
pboutill
aspiwack
herbelin
msozeau
barras
soubiran
jforest