| Age | Commit message (Expand) | Author |
|---|
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack |
| 2014-09-04 | Types declared as Variants really do not accept recursive definitions. | Arnaud Spiwack |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Fix bug when defining primitive projections mixing defined and abstracts fields. | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Complying an ocaml warning. | Hugo Herbelin |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-05-06 | Allow records whose sort is defined by a constant. | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 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 |
| 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-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-09-18 | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot |
| 2013-09-12 | Unplugging Autoinstance. The code is still here if someone wishes | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | 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-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-26 | Monomorphization (toplevel) | ppedrot |
| 2012-11-17 | Taking into account the type of a definition (if it exists), and the | herbelin |
| 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-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-04 | Separated notice vs info messages, and cleaned up the interface a bit. | ppedrot |
| 2012-06-01 | Cleaning Pp.ppnl use | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml | letouzey |
| 2012-04-13 | Better error message when defining recursive records with Record or | aspiwack |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-25 | Check for unresolved evars in textual order of the params and fields declarat... | msozeau |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-11-18 | Restore backward compatibility. ":>" declares subinstances in Class declarati... | msozeau |
