index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
* library/Library: Reformulate a comment.
regisgia
2010-08-27
*
* library/Library: Document.
regisgia
2010-08-27
*
* lib/Flags: Replace dont_load_proofs by load_proofs since not loading
regisgia
2010-08-27
*
* Improve documentation of LightenLibrary.
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing: New LightenLibrary.
regisgia
2010-08-27
*
* library/Library: Remove the use of the old-fashioned lighten_library.
regisgia
2010-08-27
*
* library/Library: Remove lighten_library definition.
regisgia
2010-08-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Some fine-tuning after removal of automatic imports of coercions in r13310
herbelin
2010-07-23
*
change the flag "internal" in declare/ind_tables from bool to
vsiles
2010-06-29
*
Moved error when option does not exist into a warning (this allows to
herbelin
2010-06-25
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Protection against anomaly when loading a state with bad magic number.
herbelin
2010-06-22
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Patch bug 2313.
soubiran
2010-05-05
*
"make source-doc" builds documentation of mli in html and pdf at
pboutill
2010-04-29
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Added a new exception for already declared Schemes,
vsiles
2010-04-27
*
Util: remove list_split_at which is a clone of list_chop
letouzey
2010-04-16
*
Granting wish #2249 (checking existing lemma name also when in a section).
herbelin
2010-04-09
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
Simplify backtracking
vgross
2010-02-12
*
Fixing closing of segments.
vgross
2010-02-12
*
Small fix on module inclusion.
soubiran
2010-02-02
*
Various bug fix on recent features of the module system:
soubiran
2010-01-19
*
Variant !F M for functor application that does not honor the Inline declarations
letouzey
2010-01-17
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
Declaremods.ml: a useless function wrongly introduced in last commit
letouzey
2009-12-08
*
No more specific syntax "Include Self" for inclusion of partially-applied fun...
letouzey
2009-12-07
*
declaremods.ml <--- code factoring
soubiran
2009-12-03
*
Continuing r12485-12486 (cleaning around name generation)
herbelin
2009-12-01
*
Now "Include Self <expr>" handles partially applied functors, cf for example ...
soubiran
2009-11-18
*
Module subtyping : allow many <: and module type declaration with <:
letouzey
2009-11-18
*
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
letouzey
2009-11-16
*
Include Self (Type) Foo: applying a (Type) Functor to the current context
letouzey
2009-11-16
*
Fixed bug #2168 (closing a section may have as side-effect the erasure
herbelin
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Undo 12432 which caused an exponential behavior at Requires. Compilation time...
puech
2009-10-30
*
Fix incorrect registration of objects in libtypes.ml when defining a module.
puech
2009-10-28
*
Same as commit 12430 but with the good version of the function iter_all_segment
soubiran
2009-10-28
*
From now SearchAbout requests search also inside INCLUDE libobject.
soubiran
2009-10-28
*
Local/Global revision 12418 continued
herbelin
2009-10-26
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
[next]