| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | 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 | 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-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-08 | Uniformizing the [if_warn] flag used for warning printing and put | ppedrot |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-11-26 | Monomorphization (toplevel) | ppedrot |
| 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-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-01 | Let's try to avoid generating induction principles for records (wish #2693) | letouzey |
| 2012-05-30 | More uniformisation in Pp.warn functions. | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Deactivated automatic inference of _case schemes, as it was in 8.3 | herbelin |
| 2011-12-17 | A pass on warning printings. Made systematic the use of msg_warning so | herbelin |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-11-24 | Added a DEPRECATED flag in declaration of options. For now only two options a... | ppedrot |
| 2011-06-13 | Another bug of Scheme Induction (generated names dep/nodep were swapped). | herbelin |
| 2011-06-13 | Fixing an anomaly in Scheme Induction. | herbelin |
| 2011-05-16 | turn the automatic generation of boolean equality | vsiles |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-02-10 | Remove obsolete TheoryList | glondu |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-09-02 | * removed declare_constant and declare_internal_constant | vsiles |
| 2010-09-02 | v13392 port from v8.3 to trunk : correct message when defining inductive schemes | vsiles |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-29 | change the flag "internal" in declare/ind_tables from bool to | vsiles |
| 2010-05-29 | New pass on inductive schemes | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-27 | Added a new exception for already declared Schemes, | vsiles |
| 2010-03-06 | Fixes in rewrite and a Elimination/Case to Scheme: | msozeau |
| 2010-03-05 | Minor fixes. | msozeau |
| 2009-12-13 | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin |
| 2009-11-09 | Quick fix for restoring a left-to-right rewriting lemma compatible | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
