| Commit message (Expand) | Author | Age |
* | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | 2014-03-05 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Fixing an incompleteness of the ring/field tactics | amahboub | 2013-08-23 |
* | Little fix for Nsatz: hypotheses not directly relevant to the nsatz | herbelin | 2013-05-05 |
* | Restrict (try...with...) to avoid catching critical exn (part 15) | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey | 2013-03-13 |
* | Unset Asymmetric Patterns | pboutill | 2013-01-18 |
* | Array.create is deprecated | pboutill | 2012-12-19 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | 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 |
* | place all files specific to camlp4 syntax extensions in grammar/ | letouzey | 2012-05-29 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Fix typo | glondu | 2012-01-12 |
* | moins de reification inutile, noatations standards | pottier | 2011-08-04 |
* | Nsatz: replaced some generic = on constr by eq_constr | puech | 2011-07-29 |
* | Ring2 devient Ncring et la reification par les type classes est partagee | pottier | 2011-07-26 |
* | Tests de nsatz avec la geometrie | pottier | 2011-06-16 |
* | ring2, cring, nsatz avec type classe avec parametres plus notations | pottier | 2011-06-10 |
* | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey | 2011-05-05 |
* | 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 |
* | Move stuff about positive into a distinct PArith subdir | letouzey | 2010-11-02 |
* | unification des tactiques nsatz pour R Z avec celle des anneaux integres | pottier | 2010-07-28 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0... | pottier | 2010-07-28 |
* | nstaz pour les anneaux integres et les setoides, R Z et Q | pottier | 2010-07-27 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Fix compilation and test-suite of nsatz | glondu | 2010-07-12 |
* | nsatz in an integral domain with specialization to Z and R | pottier | 2010-07-08 |
* | bug 2328 fixed: failure when polynomial not i ideal | pottier | 2010-06-25 |
* | Misc fixes related to new nsatz (and ocamlbuild) | letouzey | 2010-06-03 |
* | nsatz ajoute | pottier | 2010-06-03 |