| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-09-06 | Fix computation of obligations for mutually recursive definitions. | msozeau |
| 2012-08-24 | Assumption commands are now displayed as unsafe in Coqide. | aspiwack |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-12 | Bug 2838: ExplApp in mutual inductive parameters | pboutill |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-04 | Fixing previous commit (something strange happened...) | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-04 | Separated notice vs info messages, and cleaned up the interface a bit. | ppedrot |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
