index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
library
Age
Commit message (
Expand
)
Author
2012-11-22
Monomorphization (library)
ppedrot
2012-11-13
More monomorphizations
ppedrot
2012-11-08
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-10-29
Fixed #2926:
ppedrot
2012-10-29
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-26
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-06
avoid using rectypes in nametab.ml
letouzey
2012-10-02
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-09-18
Cleaning interface of Util.
ppedrot
2012-09-17
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-15
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-14
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-08-24
correct some ends of .mllib files (avoid a broken tolink.ml)
letouzey
2012-08-24
Assumption commands are now displayed as unsafe in Coqide.
aspiwack
2012-08-08
Updating headers.
herbelin
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-01
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-05-30
Getting rid of Pp.msg
ppedrot
2012-05-30
More uniformisation in Pp.warn functions.
ppedrot
2012-05-29
remove many excessive open Util & Errors in mli's
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
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-04-12
lib directory is cut in 2 cma.
pboutill
2012-03-26
Module names and constant/inductive names are now in two separate namespaces
letouzey
2012-03-23
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
Remove undocumented command "Delete foo"
letouzey
2012-03-20
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-02
Noise for nothing
pboutill
2012-02-23
Implement the substitution function for global options. Fixes anomaly in ssre...
msozeau
2011-12-21
sequel of previous commit
letouzey
2011-12-21
Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...
letouzey
2011-12-18
Fixed a Not_found bug when declaring in a section some implicit
herbelin
2011-12-17
A pass on warning printings. Made systematic the use of msg_warning so
herbelin
2011-12-12
Proof using ...
gareuselesinge
2011-12-06
Minor fixes to Arguments
gareuselesinge
2011-11-24
Added a function to inspect current option state.
ppedrot
2011-11-24
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-21
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
New Arguments vernacular
gareuselesinge
2011-11-18
Adding the type infrastructure to handle properly API management of options
ppedrot
2011-11-02
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-10-25
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-24
Heads: avoid potentially uncaught Not_found via an assert false
letouzey
2011-10-12
Temporary revert commit 14550 since it breaks a few contribs
letouzey
[prev]
[next]