index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
setoid_ring
Commit message (
Expand
)
Author
Age
*
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
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.
ppedrot
2012-06-12
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
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-05-29
*
Everything compiles again.
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Proof using ...
gareuselesinge
2011-12-12
*
Fixing bug #2640 and variants of it (inconsistency between when and
herbelin
2011-11-17
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Esubst: make types of substitutions & lifts private
puech
2011-08-08
*
moins de reification inutile, noatations standards
pottier
2011-08-04
*
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-29
*
Integral domains
pottier
2011-07-26
*
Ring2 devient Ncring et la reification par les type classes est partagee
pottier
2011-07-26
*
Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def
letouzey
2011-06-28
*
Follow-up concerning eqb / ltb / leb comparisons
letouzey
2011-06-21
*
ring2, cring, nsatz avec type classe avec parametres plus notations
pottier
2011-06-10
*
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-05-05
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Quickly avoid global axioms in Loic new files about ring
letouzey
2011-04-03
*
syntax for exponents
pottier
2011-03-08
*
Revert "syntax for exponents"
glondu
2011-02-25
*
syntax for exponents
pottier
2011-02-22
*
anneaux commutatifs ou non, reification sans ml
pottier
2011-02-22
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Integer division: quot and rem (trunc convention) in addition to div and mod
letouzey
2010-11-10
*
Still some more Cpow in Type rather than Set (cf. r13542)
letouzey
2010-10-21
*
Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)
letouzey
2010-10-14
[next]