aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2011-10-11in heads.ml, at least turn the Not_found of #2608 into assert falseletouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-09-24Completing r14448 and thus continuing r14407 (using Cast to propagateherbelin
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
2011-09-15Names.make_mbid and co : convert from/to identifier (avoid some String.copy)letouzey
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
2011-09-05Lib: remove strange code about backtracking to the current stateletouzey
2011-09-05Lib.node: merge OpenedModtype and OpenedModule, same for Closed...letouzey
2011-07-29Heads: generic equality on constr replaced by destructorpuech
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-17Goptions: repair Unset for int optionsletouzey
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-02-11Annotations at functor applications:letouzey
2011-02-10More comments and less doublons in some mlipboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-11Fix some typosglondu
2010-10-31Minor code improvements around libobjectherbelin
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Dead code in impargs (afaics, no more need, since r11242, to mergeherbelin
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 20:40:55 +0000