| Age | Commit message (Expand) | Author |
|---|
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-11-17 | Fixing bug #2640 and variants of it (inconsistency between when and | herbelin |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-08-08 | Esubst: make types of substitutions & lifts private | puech |
| 2011-08-04 | moins de reification inutile, noatations standards | pottier |
| 2011-07-29 | Newring: generic = on constr replaced by eq_constr | puech |
| 2011-07-29 | replaced some generic = on constr by eq_constr | puech |
| 2011-07-29 | Newring: replaced some generic = on constr by eq_constr | puech |
| 2011-07-29 | Newring: replaced generic = on constr by eq_constr | puech |
| 2011-07-29 | Newring: generic Pervasives.compare on constr replaced by constr_ord | puech |
| 2011-07-29 | Newring: generic equality on constr replaced by constr_equal | puech |
| 2011-07-26 | Integral domains | pottier |
| 2011-07-26 | Ring2 devient Ncring et la reification par les type classes est partagee | pottier |
| 2011-06-28 | Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def | letouzey |
| 2011-06-21 | Follow-up concerning eqb / ltb / leb comparisons | letouzey |
| 2011-06-10 | ring2, cring, nsatz avec type classe avec parametres plus notations | pottier |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | letouzey |
| 2011-05-05 | Setoid_ring: some cleanups related with BinPos and BinNat | letouzey |
| 2011-05-05 | Modularization of BinPos + fixes in Stdlib | letouzey |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-03 | Quickly avoid global axioms in Loic new files about ring | letouzey |
| 2011-03-08 | syntax for exponents | pottier |
| 2011-02-25 | Revert "syntax for exponents" | glondu |
| 2011-02-22 | syntax for exponents | pottier |
| 2011-02-22 | anneaux commutatifs ou non, reification sans ml | pottier |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-11-10 | Integer division: quot and rem (trunc convention) in addition to div and mod | letouzey |
| 2010-10-21 | Still some more Cpow in Type rather than Set (cf. r13542) | letouzey |
| 2010-10-14 | Ring : Cpow in Type rather than Set (type of power coeffs in power_theory) | letouzey |
| 2010-09-30 | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-19 | Reverting partial fix for #2335 committed by mistake in r13435. Sorry. | herbelin |
| 2010-09-19 | Patch solving the bug but leaving open design choices | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-18 | 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-16 | fixed bug #2316 (ring_simplify) | barras |
| 2010-06-06 | Added support for Ltac-matching terms with variables bound in the pattern | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-05 | Improvements in generalized rewriting: | msozeau |
| 2010-02-10 | bug in field_simplify_eq in | barras |
| 2010-02-10 | Euclidean division for NArith | letouzey |
| 2010-01-28 | New command Declare Reduction <id> := <conv_expr>. | letouzey |
