aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Minor code improvements around libobjectGravatar herbelin2010-10-31
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Dead code in impargs (afaics, no more need, since r11242, to mergeGravatar herbelin2010-10-03
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* * library/Library: Reformulate a comment.Gravatar regisgia2010-08-27
* * library/Library: Document.Gravatar regisgia2010-08-27
* * lib/Flags: Replace dont_load_proofs by load_proofs since not loadingGravatar regisgia2010-08-27
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* * library/Library: Remove the use of the old-fashioned lighten_library.Gravatar regisgia2010-08-27
* * library/Library: Remove lighten_library definition.Gravatar regisgia2010-08-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Some fine-tuning after removal of automatic imports of coercions in r13310Gravatar herbelin2010-07-23
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* Moved error when option does not exist into a warning (this allows toGravatar herbelin2010-06-25
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Protection against anomaly when loading a state with bad magic number.Gravatar herbelin2010-06-22
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Patch bug 2313.Gravatar soubiran2010-05-05
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Added a new exception for already declared Schemes, Gravatar vsiles2010-04-27
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Simplify backtrackingGravatar vgross2010-02-12
* Fixing closing of segments.Gravatar vgross2010-02-12
* Small fix on module inclusion.Gravatar soubiran2010-02-02
* Various bug fix on recent features of the module system:Gravatar soubiran2010-01-19
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Declaremods.ml: a useless function wrongly introduced in last commitGravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* declaremods.ml <--- code factoringGravatar soubiran2009-12-03
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Now "Include Self <expr>" handles partially applied functors, cf for example ...Gravatar soubiran2009-11-18
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09