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
/
newring.ml4
Commit message (
Expand
)
Author
Age
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
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
*
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
*
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
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
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
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
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-09-19
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Improvements in generalized rewriting:
msozeau
2010-03-05
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Stop unnecessary use of lazy values for constraints, simplifying
msozeau
2009-09-02
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Move setoid_rewrite to its own module and do some clean up in
msozeau
2009-04-07
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20