| Commit message (Expand) | Author | Age |
* | Retyping API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Termops API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
* | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-10-02 |
|\ |
|
| * | Fix bug #5069: Scheme Equality gives anomalies in sections. | Pierre-Marie Pédrot | 2016-10-02 |
* | | Make the user_err header an optional parameter. | Emilio Jesus Gallego Arias | 2016-08-19 |
|/ |
|
* | Renaming to more generic has_dependent_elim test | Matthieu Sozeau | 2016-07-06 |
* | Move is_prim... to Inductiveops and correct Scheme | Matthieu Sozeau | 2016-07-06 |
* | primproj: warning and avoid error. | Matthieu Sozeau | 2016-07-06 |
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | A new infrastructure for warnings. | Maxime Dénès | 2016-06-29 |
* | Reuse the typing_flags datatype for inductives. | Pierre-Marie Pédrot | 2016-06-18 |
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive. | Pierre-Marie Pédrot | 2016-06-16 |
|\ |
|
* | | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-03-09 |
|\ \ |
|
| * | | Adding backtraces to scheme error messages. | Pierre-Marie Pédrot | 2016-03-07 |
* | | | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
|/ / |
|
* | | 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 |
| * | Add corresponding field in `VernacInductive`. | Arnaud Spiwack | 2015-06-24 |
|/ |
|
* | 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 |