| Age | Commit message (Expand) | Author |
|---|
| 2010-05-02 | Fix discrimination of sorts which doesn't play well with cumulativity | msozeau |
| 2010-04-29 | 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-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-04-20 | Fixed bug #2999 (destruct was not refreshing universes of what it generalized *) | herbelin |
| 2010-04-18 | Fixed some printing bugs. | herbelin |
| 2010-04-17 | 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-16 | Util: remove list_split_at which is a clone of list_chop | letouzey |
| 2010-04-14 | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin |
| 2010-04-05 | 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-03-27 | Applied greenrd's patch to fix bug 2255 (injection failed to | herbelin |
| 2010-03-15 | Fix splitting evars tactics and stop dropping evar constraints when | msozeau |
| 2010-03-12 | fixed confusion between number of cstr arguments and number of pattern variab... | barras |
| 2010-03-07 | Fix lifting of constraints in generalized rewriting tactic. | msozeau |
| 2010-03-06 | Fixes in rewrite and a Elimination/Case to Scheme: | msozeau |
| 2010-03-05 | 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-02-10 | Fix [Existing Class] impl and add documentation. Fix computation of the | msozeau |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2010-01-26 | 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-12 | 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 |
| 2009-12-30 | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin |
| 2009-12-29 | Improving descend_in_conjunctions (using a combinators instead of a tactic) | herbelin |
| 2009-12-28 | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin |
| 2009-12-27 | Fix "Existing Instance" to handle globality information and "Existing | msozeau |
| 2009-12-24 | 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-23 | Moved a bit further the code for pattern interpretation in match goal | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-19 | Backtrack on making exact hints for lemmas starting with products | msozeau |
| 2009-12-16 | adding an option functional_induction_rewrite_dependent to make functional in... | jforest |
| 2009-12-14 | Improved strategy for rewriting lemma possibly depending because of evars. | herbelin |
| 2009-12-13 | 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-12 | 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-06 | 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-03 | Restored rewriting of JMeq using JMeq_rect and co when the domains are the same | herbelin |
| 2009-12-01 | 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 |
