| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | addition of lia.cache - csdp.cache is now handled by micromega not csdpcert | fbesson | 2009-07-31 |
| * | micromega : Better parsing of formulae - smaller proof terms for Z - redesign... | fbesson | 2009-07-30 |
| * | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey | 2009-07-24 |
| * | 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-20 |
| * | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau | 2009-07-09 |
| * | repport of commit r12221 |  jforest | 2009-07-04 |
| * | Miscellaneous practical commits: | herbelin | 2009-06-29 |
| * | Fix bug introduced by last revision, subtac_cases was returning the | msozeau | 2009-06-29 |
| * | 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-28 |
| * | Fixes for r12197, the refined evars were not returned in case fail_evar | msozeau | 2009-06-22 |
| * | Use more consistent resolution parameters in Program and regular typing | msozeau | 2009-06-18 |
| * | Fallback on not using [fix_proto] if the right imports aren't there, the | msozeau | 2009-06-17 |
| * | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
| * | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin | 2009-06-06 |
| * | Fix implicit args code so that declarations are added for all | msozeau | 2009-05-27 |
| * | Fix de Bruijn lifting bug appearing when we match on multiple terms with | msozeau | 2009-05-26 |
| * | Support for definition hooks in subtac. | msozeau | 2009-05-16 |
| * | micromega: proof compression bugfix | fbesson | 2009-05-11 |
| * | More efficient handling of evars in Program Fixpoint commands. | msozeau | 2009-04-28 |
| * | - Cleaning (unification of ML names, removal of obsolete code, | herbelin | 2009-04-27 |
herbelin
fbesson
glondu
msozeau
gmelquio
letouzey
marche
aspiwack
jforest