| Age | Commit message (Expand) | Author |
|---|
| 2016-09-26 | Monomorphizing various uses of arrays in Nsatz. | Pierre-Marie Pédrot |
| 2016-09-26 | Partial fix for bug #5085: nsatz_compute stack overflows. | Pierre-Marie Pédrot |
| 2016-07-13 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-06 | improved complexity in nsatz | thery |
| 2016-07-06 | Bug Fixes : 4851 4858 4880 for nsatz | thery |
| 2016-07-05 | Bug fix : variable capture in ltac code of Nsatz | thery |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-06-08 | Compilation via pack for plugins of the stdlib | Pierre Letouzey |
| 2016-05-16 | Put the "generalize" tactic in the monad. | Pierre-Marie Pédrot |
| 2016-03-06 | Splitting the nsatz ML module into an implementation and a grammar files. | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-08-23 | Fixing an incompleteness of the ring/field tactics | amahboub |
| 2013-05-05 | Little fix for Nsatz: hypotheses not directly relevant to the nsatz | herbelin |
| 2013-03-13 | 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-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-19 | Array.create is deprecated | pboutill |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | 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-08-08 | Updating headers. | herbelin |
| 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-06-28 | Cleaning opening of the standard List module. | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-12 | Fix typo | glondu |
| 2011-08-04 | moins de reification inutile, noatations standards | pottier |
| 2011-07-29 | Nsatz: replaced some generic = on constr by eq_constr | puech |
| 2011-07-26 | Ring2 devient Ncring et la reification par les type classes est partagee | pottier |
| 2011-06-16 | Tests de nsatz avec la geometrie | pottier |
| 2011-06-10 | ring2, cring, nsatz avec type classe avec parametres plus notations | pottier |
| 2011-05-05 | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-11-18 | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey |
| 2010-11-02 | Move stuff about positive into a distinct PArith subdir | letouzey |
| 2010-07-28 | 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-27 | nstaz pour les anneaux integres et les setoides, R Z et Q | pottier |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-12 | Fix compilation and test-suite of nsatz | glondu |
| 2010-07-08 | nsatz in an integral domain with specialization to Z and R | pottier |
