| Commit message (Expand) | Author | Age |
* | 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 |
* | MSets: a new generation of FSets | letouzey | 2009-10-13 |
* | Implicit argument of Logic.eq become maximally inserted | letouzey | 2009-10-08 |
* | Correctly do backtracking during type class resolution even if only new | msozeau | 2009-10-05 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Fix compilation errors due to last commit. | msozeau | 2009-09-15 |
* | Stop using [obligation_tactic] from Program.Tactics as the default | msozeau | 2009-09-15 |
* | Misc fixes: | msozeau | 2009-09-10 |
* | Fix the bug-ridden code used to choose leibniz or generalized | msozeau | 2009-09-08 |