aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
* Completing r14448 and thus continuing r14407 (using Cast to propagateGravatar herbelin2011-09-24
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
* Names.make_mbid and co : convert from/to identifier (avoid some String.copy)Gravatar letouzey2011-09-15
* Coqide: new backtracking code, based on the Backtrack commandGravatar letouzey2011-09-05
* Lib: remove strange code about backtracking to the current stateGravatar letouzey2011-09-05
* Lib.node: merge OpenedModtype and OpenedModule, same for Closed...Gravatar letouzey2011-09-05
* Heads: generic equality on constr replaced by destructorGravatar puech2011-07-29
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
* Annotations at functor applications:Gravatar letouzey2011-02-11
* More comments and less doublons in some mliGravatar pboutill2011-02-10
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Fix some typosGravatar glondu2011-01-11
* 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