| Commit message (Expand) | Author | Age |
* | still some more dead code removal | letouzey | 2012-10-06 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Try to make the use of Unix.lockf in micromega compatible with Win32 | letouzey | 2012-08-06 |
* | Ring_polynom : a restricted simpl instead of a unfold;fold | letouzey | 2012-07-07 |
* | Legacy Ring and Legacy Field migrated to contribs | letouzey | 2012-07-05 |
* | rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite | letouzey | 2012-07-05 |
* | More cleanup in Ring_polynom and EnvRing | letouzey | 2012-07-05 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | Cleaning opening of the standard List module. | ppedrot | 2012-06-28 |
* | More cleaning | ppedrot | 2012-06-01 |
* | place all files specific to camlp4 syntax extensions in grammar/ | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | lib directory is cut in 2 cma. | pboutill | 2012-04-12 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | coq_micromega.ml: fix order of recursive calls to rconstant | glondu | 2012-01-14 |
* | More newlines in debugging output of psatzl | glondu | 2012-01-14 |
* | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge | 2011-11-21 |
* | Coq_micromega: generic = on constr replaced by eq_constr | puech | 2011-07-29 |
* | update of Micromega doc | fbesson | 2011-06-29 |
* | improved tactic names | fbesson | 2011-06-28 |
* | Numbers: a particular case of div_unique | letouzey | 2011-06-24 |
* | Q2R -> IQR | fbesson | 2011-05-25 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0... | fbesson | 2011-05-23 |
* | added support to handle division by a constant over R | fbesson | 2011-05-20 |
* | cbv delta - [...] before calling lia | fbesson | 2011-05-18 |
* | apply zeta reduction before syntaxification | fbesson | 2011-05-18 |
* | Improved lia + experimental nlia | fbesson | 2011-05-09 |
* | Modularization of BinInt, related fixes in the stdlib | letouzey | 2011-05-05 |
* | Modularization of BinNat + fixes of stdlib | letouzey | 2011-05-05 |
* | Modularization of BinPos + fixes in Stdlib | letouzey | 2011-05-05 |
* | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey | 2011-05-05 |
* | bug fix: concurrent access of persistent_cache | fbesson | 2011-04-21 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey | 2010-11-18 |
* | Solve name conflict about pow introduced by commit 13546. | letouzey | 2010-10-21 |
* | Still some more Cpow in Type rather than Set (cf. r13542) | letouzey | 2010-10-21 |
* | Fix unescaped end-of-lines (OCaml warning 29) | glondu | 2010-09-13 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Reverted 13293 commited mistakenly. Sorry for the noise. | herbelin | 2010-07-18 |
* | Tentative de suppression de l'import automatique des hints et coercions. | herbelin | 2010-07-18 |
* | QArith: typo in name of hint db (fix #2346) | letouzey | 2010-06-29 |
* | A little bit of cleanup, and some annotations. | fkirchne | 2010-05-28 |
* | Modify the test for csdp and associated message. | fkirchne | 2010-05-28 |
* | ... | fkirchne | 2010-05-28 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Look for csdp in $PATH at runtime, remove -csdpdir configure option | glondu | 2010-04-11 |
* | Remove unused functions run_sdpa | glondu | 2010-04-11 |
* | Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i... | letouzey | 2010-03-30 |