| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Backporting 12080 (fixing bug #2091 on bad rollback in the "where" | herbelin | 2009-04-24 |
| * | - New cleaning phase for the entry points of pretyping.ml | herbelin | 2009-04-24 |
| * | Better Requires in Classes. Fix bug #2093: the code does not require | msozeau | 2009-04-16 |
| * | nouvelle version de la tactique groebner proposee par Loic: |  barras | 2009-04-16 |
| * | Experimental support for automatic destruction of recursive calls and | msozeau | 2009-04-08 |
| * | Fix bug #2083 for good: verify that the measure and relation are | msozeau | 2009-04-08 |
| * | Some dead code removal + cleanups | letouzey | 2009-04-08 |
| * | Fixes in Program: | msozeau | 2009-04-07 |
| * | Move setoid_rewrite to its own module and do some clean up in | msozeau | 2009-04-07 |
| * | Ocamlbuild: improvements suggested by N. Pouillard | letouzey | 2009-04-03 |
| * | Add a more general quote construction |  glondu | 2009-03-30 |
| * | Fix some typos and spaces | glondu | 2009-03-30 |
| * | Csdpcert: adaptation after last commit | letouzey | 2009-03-29 |
| * | Micromega: improvement of the code obtained by extraction | letouzey | 2009-03-29 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
| * | Fix static compilation of numeral syntax (typo in _mod files, sorry ...) | letouzey | 2009-03-28 |
| * | ZMicromega: useless dependency toward ZArith.Int | letouzey | 2009-03-28 |
| * | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey | 2009-03-27 |
| * | GroebnerZ: no more admitted lemmas | letouzey | 2009-03-27 |
| * | Fixes in Program well-founded definitions: | msozeau | 2009-03-26 |
| * | ocamlbuild: coqide, coqchk, a bit of .vo | letouzey | 2009-03-26 |
| * | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey | 2009-03-20 |
| * | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey | 2009-03-20 |
letouzey
msozeau
jforest
herbelin
fbesson
barras
glondu