| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-06-14 | Fixing bug #2181 (Class mechanism can create dependencies over unnamed | herbelin |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-11 | Keep information on which fields are subclasses in class declarations, | msozeau |
| 2011-02-10 | Interp a definition with the implicit arguments of its local context | pboutill |
| 2011-02-10 | Data structure telling implicits of local variables is a map in the | pboutill |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-11-18 | Do not throw an error for anonymous generalized binders as they will be | msozeau |
| 2010-11-15 | Minor fixes from Gregory Malecha. A typo fixed and a better (located) | msozeau |
