| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-25 | Removing Autoinstance once and for all. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2013-12-30 | Useless Evd.create_evar_defs. | Pierre-Marie Pédrot |
| 2013-12-24 | STM: capture type checking error (Closes: 3195) | Enrico Tassi |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-03 | Fixup bug 3145 | pboutill |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-31 | Future: better doc + restore ~pure optimization | gareuselesinge |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-18 | declaration_hooks use Ephemeron | gareuselesinge |
| 2013-10-18 | Future: ported to Ephemeron + exception enhancing | gareuselesinge |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-18 | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot |
| 2013-08-08 | get rid of closures in global/proof state | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | Use definition_entry to declare local definitions | gareuselesinge |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-09 | Uniformization: isevars -> evdref/sigma/evd | herbelin |
| 2013-05-09 | Fixing r16487 on sharing evars between multiple parameters (missing List.rev). | herbelin |
| 2013-05-08 | Uniformizing the [if_warn] flag used for warning printing and put | ppedrot |
| 2013-05-08 | Declaration of multiple hypotheses or parameters now share typing | herbelin |
| 2013-05-08 | Share more information between constructors and arity of an inductive | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-22 | Fix bug# 2994, 2971 about better error messages. | msozeau |
| 2013-03-18 | Making local variable warning verbose by default. | ppedrot |
| 2013-03-13 | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-12-14 | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot |
| 2012-11-26 | Monomorphization (toplevel) | 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-18 | Cleaning interface of Util. | ppedrot |
| 2012-09-15 | Some documentation and cleaning of CList and Util interfaces. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
