| Commit message (Expand) | Author | Age |
* | Fixup bug 3145 | pboutill | 2013-11-03 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Future: better doc + restore ~pure optimization | gareuselesinge | 2013-10-31 |
* | Conv_orable made functional and part of pre_env | gareuselesinge | 2013-10-31 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
* | cList: set-as-list functions are now with an explicit comparison | letouzey | 2013-10-23 |
* | declaration_hooks use Ephemeron | gareuselesinge | 2013-10-18 |
* | Future: ported to Ephemeron + exception enhancing | gareuselesinge | 2013-10-18 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot | 2013-09-18 |
* | get rid of closures in global/proof state | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | 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-09 |
* | 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-05-08 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Fix bug# 2994, 2971 about better error messages. | msozeau | 2013-03-22 |
* | Making local variable warning verbose by default. | ppedrot | 2013-03-18 |
* | 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-13 |
* | 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-03-11 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | 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-12-14 |
* | Monomorphization (toplevel) | ppedrot | 2012-11-26 |
* | 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 |
* | Cleaning interface of Util. | ppedrot | 2012-09-18 |
* | Some documentation and cleaning of CList and Util interfaces. | ppedrot | 2012-09-15 |
* | 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-14 |
* | Fix computation of obligations for mutually recursive definitions. | msozeau | 2012-09-06 |
* | Assumption commands are now displayed as unsafe in Coqide. | aspiwack | 2012-08-24 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Bug 2838: ExplApp in mutual inductive parameters | pboutill | 2012-07-12 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | 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 | 2012-06-04 |