| Commit message (Expand) | Author | Age |
* | 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 |
* | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey | 2009-11-12 |
* | Promote evar_defs to evar_map (in Evd) | glondu | 2009-11-11 |
* | Added support for multiple where-clauses in Inductive and co (see wish #2163). | herbelin | 2009-11-11 |
* | use only why-dp, support for z3 | marche | 2009-11-10 |
* | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names. | gmelquio | 2009-11-04 |
* | OrderedType implementation for various numerical datatypes + min/max structures | letouzey | 2009-11-03 |
* | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
* | Make usage of Dyn explicit | glondu | 2009-10-28 |
* | Add a new vernacular command for controling implicit generalization of | msozeau | 2009-10-27 |
* | New cleaning phase of the Local/Global option management | herbelin | 2009-10-26 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |
* | Fix bug #2162 and a name clashing bug in generalized binders. | msozeau | 2009-10-09 |
* | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey | 2009-10-08 |
* | Fix for missing hypotesae in XML proof tree export. | cek | 2009-10-07 |
* | Removal of trailing spaces. | serpyc | 2009-10-04 |
* | Fixed small name freshness bug in Functional Scheme ("Heq" name was | herbelin | 2009-10-03 |
* | Add support for Local Declare ML Module | glondu | 2009-09-29 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin | 2009-09-20 |
* | micromega: better handling of exponentiation + correction of test-suite termi... | fbesson | 2009-09-18 |
* | Remove useless Liboject.export_function field | glondu | 2009-09-17 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Dont't forget to update the state or an obligation tactic assignment may | msozeau | 2009-09-15 |
* | Stop using [obligation_tactic] from Program.Tactics as the default | msozeau | 2009-09-15 |
* | Backtrack on the forced discharge of type class variables introduced | msozeau | 2009-09-14 |
* | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin | 2009-09-13 |
* | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
* | Removed Gappa from the external provers supported by the dp plugin. Tactic ga... | gmelquio | 2009-09-11 |
* | - Resolve type class constraints before trying to find unresolved | msozeau | 2009-09-11 |
* | Misc fixes: | msozeau | 2009-09-10 |
* | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
* | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
* | ajout CVC3; ajout traduction des reels | marche | 2009-09-07 |
* | Stop unnecessary use of lazy values for constraints, simplifying | msozeau | 2009-09-02 |
* | Hack to correctly get ill-formed rec body exceptions even | msozeau | 2009-09-02 |
* | update for why 2.19 | marche | 2009-08-28 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0... | fbesson | 2009-08-25 |
* | new csdp cache + improved error message | fbesson | 2009-08-20 |
* | new csdp cache + improved error message | fbesson | 2009-08-20 |
* | +Fix interface. | aspiwack | 2009-08-14 |
* | Death of "survive_module" and "survive_section" (the first one was | herbelin | 2009-08-13 |
* | Infix (r12268 continued) | herbelin | 2009-08-11 |
* | Cleaning of Nametab continued + fixed a compilation bug in previous commit. | herbelin | 2009-08-06 |
* | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
* | Added "etransitivity". | herbelin | 2009-08-03 |
* | Improved parameterization of Coq: | herbelin | 2009-08-02 |