| Commit message (Expand) | Author | Age |
* | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau | 2012-03-20 |
* | Fix bugs related to Program integration. | msozeau | 2012-03-19 |
* | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau | 2012-03-14 |
* | Everything compiles again. | msozeau | 2012-03-14 |
* | Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi... | msozeau | 2012-01-31 |
* | Tentative to fix bug #2628 by not letting intuition break records. Might be t... | msozeau | 2012-01-28 |
* | Added the decidability of (<=) on nat. | ppedrot | 2012-01-13 |
* | Fixed the itarget of the previous commit... | ppedrot | 2012-01-06 |
* | Added a typeclass-based system to reason on decidable propositions. | ppedrot | 2012-01-06 |
* | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Fix bug #2586 and enhance clsubst* as well as a side effect | msozeau | 2011-10-18 |
* | Proper fix for complement/flip instances. | msozeau | 2011-10-10 |
* | Fix bug #2557 and an issue with Propers for complement | msozeau | 2011-10-07 |
* | Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons... | letouzey | 2011-10-05 |
* | Avoid registering λ and Π as keywords just for some private Local Notation | letouzey | 2011-09-06 |
* | StrictOrder marked explicitly to be in Prop | letouzey | 2011-07-04 |
* | Merge branch 'subclasses' into coq-trunk | msozeau | 2011-05-05 |
* | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
* | - Allow rewriting under abitrary products, not just those in Prop. | msozeau | 2011-02-28 |
* | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau | 2011-01-11 |
* | f_equiv : a clone of f_equal that handles setoid equivalences | letouzey | 2011-01-04 |
* | Numbers: some improvements in proofs | letouzey | 2011-01-03 |
* | First release of Vector library. | pboutill | 2010-12-10 |
* | In passing, very quick uniformization of coqdoc headers in a few files. | herbelin | 2010-12-09 |
* | Fixed commit r13359 which was incomplete for its "trunk" part. Thanks | herbelin | 2010-07-31 |
* | Minor fixes: | msozeau | 2010-07-27 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
* | 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 |
* | RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistencies | letouzey | 2010-02-17 |
* | Cleanup in Classes, removing unsupported code. | msozeau | 2010-02-11 |
* | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey | 2010-02-09 |
* | 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 |
* | Support "Local Obligation Tactic" (now the default in sections). | msozeau | 2010-01-11 |
* | RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd | letouzey | 2009-12-18 |
* | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
* | Rename proper to proper_prf to avoid clash with CoRN, | msozeau | 2009-12-03 |
* | Fix backtracking heuristic in typeclass resolution. | msozeau | 2009-11-30 |
* | Added support for definition of fixpoints using tactics. | herbelin | 2009-11-27 |
* | Document Generalizable Variables, and change syntax to | msozeau | 2009-11-15 |
* | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
* | Numbers: finish files NStrongRec and NDefOps | letouzey | 2009-11-06 |
* | OrderedType implementation for various numerical datatypes + min/max structures | letouzey | 2009-11-03 |
* | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
* | list, length, app are migrated from List to Datatypes | letouzey | 2009-11-02 |
* | Add a new vernacular command for controling implicit generalization of | msozeau | 2009-10-27 |
* | Fix new instances that could easily make class resolution loop on | msozeau | 2009-10-22 |