| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2009-04-24 | 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-16 | 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-08 | 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-07 | Fixes in Program: | msozeau |
| 2009-04-07 | Move setoid_rewrite to its own module and do some clean up in | msozeau |
| 2009-04-03 | Ocamlbuild: improvements suggested by N. Pouillard | letouzey |
| 2009-03-30 | Add a more general quote construction | glondu |
| 2009-03-30 | Fix some typos and spaces | glondu |
| 2009-03-29 | Csdpcert: adaptation after last commit | letouzey |
| 2009-03-29 | Micromega: improvement of the code obtained by extraction | letouzey |
| 2009-03-28 | 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-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
| 2009-03-27 | GroebnerZ: no more admitted lemmas | letouzey |
| 2009-03-26 | Fixes in Program well-founded definitions: | msozeau |
| 2009-03-26 | ocamlbuild: coqide, coqchk, a bit of .vo | letouzey |
| 2009-03-20 | 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 |
