| Commit message (Expand) | Author | Age |
* | Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" w... | xclerc | 2013-10-16 |
* | Remove some uses of local modules (some were unused, some were costly). | xclerc | 2013-10-14 |
* | Getting rid of the use of deprecated elements (from the OCaml standard library). | xclerc | 2013-10-14 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Misc changes around coqtop.ml : | letouzey | 2013-08-22 |
* | micromega: remove empty file CheckerMaker | letouzey | 2013-08-22 |
* | Restrict (try...with...) to avoid catching critical exn (part 15) | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 11) | letouzey | 2013-03-13 |
* | invalid_arg instead of raise (Invalid_argement ...) | letouzey | 2013-03-12 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Unset Asymmetric Patterns | pboutill | 2013-01-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Ensure that a function declared with a label is used with it | letouzey | 2012-12-08 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | 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 |