| Age | Commit message (Expand) | Author |
|---|
| 2009-11-11 | Redoing broken commit r12498 (fixing bug #2167 + attempt to test the | herbelin |
| 2009-11-11 | Fixing bug #2167 + attempt to test the compatibility of a more robust | herbelin |
| 2009-11-11 | Test for bug #2168, forgotten in r12496. | herbelin |
| 2009-11-11 | Fixed bug #2168 (closing a section may have as side-effect the erasure | herbelin |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-11-10 | Compatibility ocaml <= 3.09 | herbelin |
| 2009-11-10 | Correction du bug #2183 | notin |
| 2009-11-10 | use only why-dp, support for z3 | marche |
| 2009-11-10 | SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax | letouzey |
| 2009-11-10 | Simplification of Numbers, mainly thanks to Include | letouzey |
| 2009-11-10 | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey |
| 2009-11-09 | Deactivation of (intrusive) printing of abbreviations from non-imported modules. | herbelin |
| 2009-11-09 | Commit 12485 continued. | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-09 | 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-08 | 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-06 | - 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-05 | 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-04 | 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-03 | 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-02 | 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-10-30 | 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-29 | Hopefully improved layout of fix guardness error message. | herbelin |
