| Age | Commit message (Expand) | Author |
|---|
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-12 | Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files. | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 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 |
