| Commit message (Expand) | Author | Age |
... | |
* | Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions... | notin | 2009-11-12 |
* | Oops, nf_evar_defs just changed to nf_evar_map. | msozeau | 2009-11-12 |
* | Don't forget to normalize everything w.r.t. evars (fixes bug #2103). | msozeau | 2009-11-12 |
* | Restore test-suite/csdp.cache erased from svn by mistake | letouzey | 2009-11-12 |
* | BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504) | letouzey | 2009-11-12 |
* | Experiment propagation of implicit arguments and arguments scope for | herbelin | 2009-11-12 |
* | Addendum to revision 12501. | herbelin | 2009-11-12 |
* | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey | 2009-11-12 |
* | Better compatibility for Peqb | letouzey | 2009-11-11 |
* | Promote evar_defs to evar_map (in Evd) | glondu | 2009-11-11 |
* | Backtracking on the use of automatically generated schemes for | herbelin | 2009-11-11 |
* | Added support for multiple where-clauses in Inductive and co (see wish #2163). | herbelin | 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-11 |
* | 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-10 |
* | 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-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 |