| Age | Commit message (Expand) | Author |
|---|
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-09-28 | Remove "init" label from Termops.it_mk* specialized functions | glondu |
| 2010-09-24 | 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-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-19 | Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we | herbelin |
| 2010-09-02 | * removed declare_constant and declare_internal_constant | vsiles |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-30 | Fix generalize_eqs tactic to not consider defined variables as being generali... | msozeau |
| 2010-06-29 | Made tclABSTRACT normalize evars before saying it does not support | herbelin |
| 2010-06-13 | Made intros_until and onInductionArg a bit stricter and robust | herbelin |
| 2010-06-09 | Relaxed the freshness constraint in "intro H" (with "H" explicit): | herbelin |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 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-14 | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2010-01-12 | 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 |
| 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-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-13 | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin |
| 2009-12-01 | Fix bug in typeclass resolution. Better handling of universes in | msozeau |
| 2009-11-24 | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-11-06 | - Fix discharge bug in typeclasses: some constrs were not actually | msozeau |
| 2009-11-06 | Misc fixes. | msozeau |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-25 | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin |
| 2009-10-25 | Add support for remaining side-conditions in "apply in as". | herbelin |
| 2009-10-04 | Changed the way to support compatibility with previous versions. | herbelin |
| 2009-10-04 | Removal of trailing spaces. | serpyc |
| 2009-10-03 | Added option "Unset Dependent Propositions Elimination" to protect | herbelin |
| 2009-09-27 | Delay the choice of eliminator in destruct/induction until we know if | herbelin |
| 2009-09-20 | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-04 | - Add more precise error localisation when one of the application fails | herbelin |
