| Commit message (Expand) | Author | Age |
|---|
| * | Moved allow_K to a unification flag |  herbelin | 2011-06-10 |
| * | Fixing another bug with "_" intro pattern. | herbelin | 2011-06-10 |
| * | Fixing the "buggy" first_name and prepare multi-induction. | herbelin | 2011-06-10 |
| * | Made use of "_" in repeated use of intros_patterns work (with | herbelin | 2011-06-10 |
| * | Integrating onLastHypId into intro so that we can get the introduction | herbelin | 2011-06-10 |
| * | Fixing commit r14061 (changes in file tactics.ml were mistakenly committed). | herbelin | 2011-04-26 |
| * | Fixing and completing interpretation of let's in notations for iterated binders. | herbelin | 2011-04-25 |
| * | Fixed a bug of destruct which was sometimes forgetting local definitions behi... | herbelin | 2011-04-24 |
| * | Add a flag to control betaiota reduction during unification to maintain backw... |  msozeau | 2011-04-18 |
| * | - Remove create_evar_defs | msozeau | 2011-04-13 |
| * | Applying Tom Prince's patch for build_constant_by_tactic not able to | herbelin | 2011-04-08 |
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| * | - Allow to set a particular transparent_state for the local hint | msozeau | 2011-03-04 |
| * | A fine-grain control of inlining at functor application via priority levels |  letouzey | 2011-01-31 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
| * | Remove "init" label from Termops.it_mk* specialized functions | glondu | 2010-09-28 |
| * | Solving bug #2212 (unification under tuples now not allowed for | herbelin | 2010-09-24 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Added eta-expansion in kernel, type inference and tactic unification, | herbelin | 2010-09-20 |
| * | Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we | herbelin | 2010-09-19 |
| * | * removed declare_constant and declare_internal_constant |  vsiles | 2010-09-02 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Fix generalize_eqs tactic to not consider defined variables as being generali... | msozeau | 2010-06-30 |
| * | Made tclABSTRACT normalize evars before saying it does not support | herbelin | 2010-06-29 |
| * | Made intros_until and onInductionArg a bit stricter and robust | herbelin | 2010-06-13 |
| * | Relaxed the freshness constraint in "intro H" (with "H" explicit): | herbelin | 2010-06-09 |
| * | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 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 |
| * | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin | 2010-04-14 |
| * | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau | 2010-01-30 |
| * | New version of 12650 that was broken (supporting again records when | herbelin | 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 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin | 2009-12-13 |
| * | Fix bug in typeclass resolution. Better handling of universes in | msozeau | 2009-12-01 |
| * | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau | 2009-11-24 |
| * | Promote evar_defs to evar_map (in Evd) | glondu | 2009-11-11 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
| * | - Fix discharge bug in typeclasses: some constrs were not actually | msozeau | 2009-11-06 |
| * | Misc fixes. | msozeau | 2009-11-06 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
| * | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin | 2009-10-25 |
herbelin
msozeau
letouzey
glondu
vsiles
aspiwack