| Commit message (Expand) | Author | Age |
|---|
| * | Adding backtraces to scheme error messages. |  Pierre-Marie Pédrot | 2016-03-07 |
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| * | Univs: generation of induction schemes should not generated useless |  Matthieu Sozeau | 2015-11-20 |
| * | Univs: local names handling. | Matthieu Sozeau | 2015-10-28 |
| * | Avoid type checking private_constants (side_eff) again during Qed (#4357). |  Enrico Tassi | 2015-10-28 |
| * | Univs: fix environment handling in scheme building. | Matthieu Sozeau | 2015-10-02 |
| * | Hopefully better names to constructors of internal_flag, as discussed |  Hugo Herbelin | 2015-09-23 |
| * | Improving over 26aa224293 in reporting unexpected error during scheme creation. | Hugo Herbelin | 2015-07-27 |
| * | Fixing bug #3736 (anomaly instead of error/warning/silence on | Hugo Herbelin | 2015-07-27 |
| * | Equality Schemes options: reverting commit ff9f94634 which is | Hugo Herbelin | 2015-01-24 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | better error message | Enrico Tassi | 2014-09-16 |
| * | Type definitions with [Variant] don't generate inductive schemes by default. |  Arnaud Spiwack | 2014-09-04 |
| * | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | 2014-09-04 |
| * | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
| * | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
| * | Making code and doc agree on "Set Equality Schemes" (see also bug #2550). | Hugo Herbelin | 2014-07-01 |
| * | Safer entry point of primitive projections in the kernel, now it does recognize |  Matthieu Sozeau | 2014-06-17 |
| * | - 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 | 2014-05-06 |
| * | Qed: feedback when type checking is done | Enrico Tassi | 2013-12-24 |
| * | More monomorphic List.mem + List.assoc + ... |  letouzey | 2013-10-24 |
| * | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey | 2013-10-23 |
| * | State Transaction Machine |  gareuselesinge | 2013-08-08 |
| * | Uniformizing the [if_warn] flag used for warning printing and put |  ppedrot | 2013-05-08 |
| * | Minor code cleaning in CArray / CList. | ppedrot | 2013-03-23 |
| * | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey | 2013-03-13 |
| * | invalid_arg instead of raise (Invalid_argement ...) | letouzey | 2013-03-12 |
| * | New implementation of the conversion test, using normalization by evaluation to |  mdenes | 2013-01-22 |
| * | Monomorphization (toplevel) | ppedrot | 2012-11-26 |
| * | 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-09-14 |
| * | Updating headers. |  herbelin | 2012-08-08 |
| * | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
| * | Replacing some str with strbrk | ppedrot | 2012-06-04 |
| * | Let's try to avoid generating induction principles for records (wish #2693) | letouzey | 2012-06-01 |
| * | More uniformisation in Pp.warn functions. | ppedrot | 2012-05-30 |
| * | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | 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-17 |
| * | Proof using ... | gareuselesinge | 2011-12-12 |
| * | Added a DEPRECATED flag in declaration of options. For now only two options a... | ppedrot | 2011-11-24 |
| * | Another bug of Scheme Induction (generated names dep/nodep were swapped). | herbelin | 2011-06-13 |
| * | Fixing an anomaly in Scheme Induction. | herbelin | 2011-06-13 |
| * | turn the automatic generation of boolean equality |  vsiles | 2011-05-16 |
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Enrico Tassi
Hugo Herbelin
Arnaud Spiwack
Matthieu Sozeau
letouzey
gareuselesinge
ppedrot
mdenes
regisgia
herbelin
pboutill
vsiles