| Age | Commit message (Expand) | Author |
|---|
| 2014-09-02 | Fix Declaremods.end_library (Closes: #3536) | Enrico Tassi |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-21 | When discharging polymorphic definitions, we must take into account all | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-26 | New compilation mode -vi2vo | Enrico Tassi |
| 2014-01-05 | STM: modules do not prevent proofs from being ASync | Enrico Tassi |
| 2013-11-07 | Partial application hunt. | ppedrot |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-12 | Minimal implementation of `Shallow marshalling of Lib | gareuselesinge |
| 2013-08-22 | Nicer code concerning dirpaths and modpath around Lib | letouzey |
| 2013-08-20 | Safe_typing code refactoring | letouzey |
| 2013-08-08 | enhance marshallable option for freeze (minor TODO in safe_typing) | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-07-17 | Lib.contents () instead of Lib.contents_after None | letouzey |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-06 | States: frozen states can hold closures | gareuselesinge |
| 2013-04-23 | Fix issues with "Reset Initial" in scripts given to coqtop -l | letouzey |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-02-19 | avoid (Int.equal (cmp ...) 0) when a boolean equality exists | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-19 | module_path --> ModPath.t, kernel_name --> KerName.t | letouzey |
| 2013-02-19 | Names: revised representation of constants and mutual_inductive | letouzey |
| 2013-02-18 | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-18 | Modulification of mod_bound_id | ppedrot |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-22 | Monomorphization (library) | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-08-24 | Assumption commands are now displayed as unsafe in Coqide. | aspiwack |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-23 | Remove undocumented command "Delete foo" | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-09-15 | Names.make_mbid and co : convert from/to identifier (avoid some String.copy) | letouzey |
| 2011-09-05 | Coqide: new backtracking code, based on the Backtrack command | letouzey |
| 2011-09-05 | Lib: remove strange code about backtracking to the current state | letouzey |
| 2011-09-05 | Lib.node: merge OpenedModtype and OpenedModule, same for Closed... | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-05 | Patch bug 2313. | soubiran |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
