aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
Commit message (Expand)AuthorAge
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* When discharging polymorphic definitions, we must take into account allGravatar Matthieu Sozeau2014-06-21
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
* Partial application hunt.Gravatar ppedrot2013-11-07
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Minimal implementation of `Shallow marshalling of LibGravatar gareuselesinge2013-09-12
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Safe_typing code refactoringGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Fix issues with "Reset Initial" in scripts given to coqtop -lGravatar letouzey2013-04-23
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (library)Gravatar ppedrot2012-11-22
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
* Noise for nothingGravatar pboutill2012-03-02
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* 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
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Patch bug 2313.Gravatar soubiran2010-05-05