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
*
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
*
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-23
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fixed a bug introduced in revision 12265.
herbelin
2009-10-08
*
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-10-06
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fix typos in comments
glondu
2009-09-17
*
Backtrack on the forced discharge of type class variables introduced
msozeau
2009-09-14
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Correction bug 2140.
soubiran
2009-08-27
[next]