aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-08-27* 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 loadingregisgia
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-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-25Moved error when option does not exist into a warning (this allows toherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-03Added command "Locate Ltac qid".herbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-05Patch bug 2313.soubiran
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-27Added a new exception for already declared Schemes, vsiles
2010-04-16Util: remove list_split_at which is a clone of list_chopletouzey
2010-04-09Granting wish #2249 (checking existing lemma name also when in a section).herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-02-12Simplify backtrackingvgross
2010-02-12Fixing closing of segments.vgross
2010-02-02Small fix on module inclusion.soubiran
2010-01-19Various bug fix on recent features of the module system:soubiran
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2009-12-08Declaremods.ml: a useless function wrongly introduced in last commitletouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-12-03declaremods.ml <--- code factoringsoubiran
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-18Now "Include Self <expr>" handles partially applied functors, cf for example ...soubiran
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
2009-11-11Fixed bug #2168 (closing a section may have as side-effect the erasureherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-30Undo 12432 which caused an exponential behavior at Requires. Compilation time...puech
2009-10-28Fix incorrect registration of objects in libtypes.ml when defining a module.puech
2009-10-28Same as commit 12430 but with the good version of the function iter_all_segmentsoubiran
2009-10-28From now SearchAbout requests search also inside INCLUDE libobject.soubiran
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 16:08:42 +0000