| Age | Commit message (Expand) | Author |
|---|
| 2009-09-20 | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin |
| 2009-09-18 | micromega: better handling of exponentiation + correction of test-suite termi... | fbesson |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-15 | 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-14 | Backtrack on the forced discharge of type class variables introduced | msozeau |
| 2009-09-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-09-11 | 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-10 | Misc fixes: | msozeau |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-09-09 | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey |
| 2009-09-07 | ajout CVC3; ajout traduction des reels | marche |
| 2009-09-02 | 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-08-28 | update for why 2.19 | marche |
| 2009-08-25 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0... | fbesson |
| 2009-08-20 | new csdp cache + improved error message | fbesson |
| 2009-08-20 | new csdp cache + improved error message | fbesson |
| 2009-08-14 | +Fix interface. | aspiwack |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-11 | Infix (r12268 continued) | herbelin |
| 2009-08-06 | 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-03 | Added "etransitivity". | herbelin |
| 2009-08-02 | Improved parameterization of Coq: | herbelin |
| 2009-07-31 | addition of lia.cache - csdp.cache is now handled by micromega not csdpcert | fbesson |
| 2009-07-30 | micromega : Better parsing of formulae - smaller proof terms for Z - redesign... | fbesson |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-07-20 | Use camlp4 to accept some specific non-exhaustive patterns in groebner | letouzey |
| 2009-07-20 | Move some examples for groebner into a test-suite file | letouzey |
| 2009-07-09 | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau |
| 2009-07-04 | repport of commit r12221 | jforest |
| 2009-06-29 | Miscellaneous practical commits: | herbelin |
| 2009-06-29 | Fix bug introduced by last revision, subtac_cases was returning the | msozeau |
| 2009-06-28 | Abstract the tycon by the matched terms when turning them into variables | msozeau |
| 2009-06-28 | Improve return predicate inference by making the return type dependent | msozeau |
| 2009-06-22 | Fixes for r12197, the refined evars were not returned in case fail_evar | msozeau |
| 2009-06-18 | Use more consistent resolution parameters in Program and regular typing | msozeau |
| 2009-06-17 | Fallback on not using [fix_proto] if the right imports aren't there, the | msozeau |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
| 2009-05-27 | Fix implicit args code so that declarations are added for all | msozeau |
| 2009-05-26 | Fix de Bruijn lifting bug appearing when we match on multiple terms with | msozeau |
| 2009-05-16 | Support for definition hooks in subtac. | msozeau |
| 2009-05-11 | micromega: proof compression bugfix | fbesson |
| 2009-04-28 | More efficient handling of evars in Program Fixpoint commands. | msozeau |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
