| Commit message (Expand) | Author | Age |
... | |
* | Quick fix for restoring a left-to-right rewriting lemma compatible | herbelin | 2009-11-09 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0... | fbesson | 2009-11-09 |
* | Fixed "Scheme Equality" when another instance of the scheme on the | herbelin | 2009-11-08 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Took local definitions into account in the test for deciding whether | herbelin | 2009-11-08 |
* | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
* | - Fix discharge bug in typeclasses: some constrs were not actually | msozeau | 2009-11-06 |
* | Datatypes.length and app defined back via fun+fix instead of Fixpoint | letouzey | 2009-11-06 |
* | Numbers: finish files NStrongRec and NDefOps | letouzey | 2009-11-06 |
* | Numbers: more (syntactic) changes toward new style of type classes | letouzey | 2009-11-06 |
* | Misc fixes. | msozeau | 2009-11-06 |
* | Changement de la version minimale requise de OCaml (3.07 => 3.09.3). | notin | 2009-11-05 |
* | Correction du bug #2142 | notin | 2009-11-05 |
* | Correction du bug #2153 (-D n'est pas une option standard de install) | notin | 2009-11-05 |
* | Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names. | gmelquio | 2009-11-04 |
* | Removed 'Toplevel' language from extraction documentation, since it is not cu... | gmelquio | 2009-11-04 |
* | Report de la révision #12208 de la v8.2 (correction du bug #2126) | notin | 2009-11-03 |
* | Removed debugging stuff mistakenly introduced in r12426. | herbelin | 2009-11-03 |
* | Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc | letouzey | 2009-11-03 |
* | ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType. | letouzey | 2009-11-03 |
* | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey | 2009-11-03 |
* | OrderedType implementation for various numerical datatypes + min/max structures | letouzey | 2009-11-03 |
* | Reverted an incorrect code simplification in function status_changed | herbelin | 2009-11-02 |
* | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey | 2009-11-02 |
* | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
* | Added alternate versions of existing lemmas on sqrt. | gmelquio | 2009-11-02 |
* | Correction du bug #2175 | notin | 2009-11-02 |
* | Sorting/Permutation: no need to require the whole Arith (and hence plugins li... | letouzey | 2009-11-02 |
* | Operators_Properties: avoid to depend on Setoid | letouzey | 2009-11-02 |
* | list, length, app are migrated from List to Datatypes | letouzey | 2009-11-02 |
* | Undo 12432 which caused an exponential behavior at Requires. Compilation time... | puech | 2009-10-30 |
* | Attempt to capture on time unification errors for "with" bindings. | herbelin | 2009-10-30 |
* | Take constraints into account in the "instantiate" tactic | herbelin | 2009-10-30 |
* | Added Coqide highlighting for extraction vernacular. | gmelquio | 2009-10-30 |
* | Removed 'dest' from keyword highlighting. | gmelquio | 2009-10-30 |
* | Hopefully improved layout of fix guardness error message. | herbelin | 2009-10-29 |
* | Fix flat_map definition so that it plays nicely with fix | glondu | 2009-10-29 |
* | Fixed some typos in the reference manual. | gmelquio | 2009-10-29 |
* | Revision 12439 continued, printing part (notations to names behave | herbelin | 2009-10-29 |
* | Fix bug in dnet.ml, which missed some results when filtering one term against... | puech | 2009-10-29 |
* | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
* | Made that notations to names behave like the names they refer to wrt | herbelin | 2009-10-28 |
* | Fixed a bug when reporting unexisting reference to an inductive | herbelin | 2009-10-28 |
* | Clarification in comments | glondu | 2009-10-28 |
* | Remove old compatibility stuff (Tacred.nf) | glondu | 2009-10-28 |
* | Make usage of Dyn explicit | glondu | 2009-10-28 |
* | Backport fix for indexing of sorts which collapse every Type occurrence | msozeau | 2009-10-28 |
* | Typo in the refman | puech | 2009-10-28 |
* | Fix incorrect registration of objects in libtypes.ml when defining a module. | puech | 2009-10-28 |
* | Same as commit 12430 but with the good version of the function iter_all_segment | soubiran | 2009-10-28 |