| Commit message (Expand) | Author | Age |
* | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
* | New compilation mode -vi2vo | Enrico Tassi | 2014-02-26 |
* | STM: modules do not prevent proofs from being ASync | Enrico Tassi | 2014-01-05 |
* | Partial application hunt. | ppedrot | 2013-11-07 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Minimal implementation of `Shallow marshalling of Lib | gareuselesinge | 2013-09-12 |
* | Nicer code concerning dirpaths and modpath around Lib | letouzey | 2013-08-22 |
* | Safe_typing code refactoring | letouzey | 2013-08-20 |
* | enhance marshallable option for freeze (minor TODO in safe_typing) | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Lib.contents () instead of Lib.contents_after None | letouzey | 2013-07-17 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | States: frozen states can hold closures | gareuselesinge | 2013-05-06 |
* | Fix issues with "Reset Initial" in scripts given to coqtop -l | letouzey | 2013-04-23 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | 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-19 |
* | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey | 2013-02-18 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Modulification of mod_bound_id | ppedrot | 2012-12-18 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Modulification of dir_path | ppedrot | 2012-12-14 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (library) | ppedrot | 2012-11-22 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | Assumption commands are now displayed as unsafe in Coqide. | aspiwack | 2012-08-24 |
* | Updating headers. | herbelin | 2012-08-08 |
* | 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-05-29 |
* | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey | 2012-03-23 |
* | Remove undocumented command "Delete foo" | letouzey | 2012-03-23 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Add type annotations around all calls to Libobject.declare_object | letouzey | 2011-11-02 |
* | Names.make_mbid and co : convert from/to identifier (avoid some String.copy) | letouzey | 2011-09-15 |
* | 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 | 2011-09-05 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Patch bug 2313. | soubiran | 2010-05-05 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Granting wish #2249 (checking existing lemma name also when in a section). | herbelin | 2010-04-09 |
* | Simplify backtracking | vgross | 2010-02-12 |
* | Fixing closing of segments. | vgross | 2010-02-12 |
* | Fixed bug #2168 (closing a section may have as side-effect the erasure | herbelin | 2009-11-11 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |