| Age | Commit message (Expand) | Author |
|---|
| 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 |
