| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-20 | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | |
| 2017-07-20 | Merge PR #903: Documenting the purity / marshallability invariant of ↵ | Maxime Dénès | |
| persistent states. | |||
| 2017-07-20 | Documenting the purity / marshallability invariant of persistent states. | Pierre-Marie Pédrot | |
| 2017-07-20 | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Maxime Dénès | |
| 2017-07-20 | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker | Maxime Dénès | |
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | |
| 2017-07-20 | Merge PR #877: Travis+4.05.0 | Maxime Dénès | |
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-19 | Removing testing unsupported Next. | Hugo Herbelin | |
| 2017-07-19 | Merge PR #745: Add timing scripts | Maxime Dénès | |
| 2017-07-19 | Merge PR #855: Deprecate options that were introduced for compatibility with ↵ | Maxime Dénès | |
| 8.5. | |||
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-19 | [proofs] Remove circular dependency from Proofview to Goal. | Emilio Jesus Gallego Arias | |
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | |
| We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | |||
| 2017-07-19 | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | |
| 2017-07-19 | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | |
| Fix bug introduced by a Haskell programmer. | |||
| 2017-07-19 | Fix debug trace of typeclasses eauto. | Théo Zimmermann | |
| 2017-07-19 | Fixing the checker w.r.t. wrongly used abstract universe contexts. | Pierre-Marie Pédrot | |
| It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker. | |||
| 2017-07-19 | Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true. | Maxime Dénès | |
| 2017-07-18 | Improve do_split option of typeclass resolution | Matthieu Sozeau | |
| It used to compute the dependencies of all undefined evars of the evar_map, while only the dependencies of resolvable evars are necessary. | |||
| 2017-07-18 | [ci] VST is now built with IGNORECOQVERSION=true. | Théo Zimmermann | |
| 2017-07-18 | Fixing a little location bug with recursive binders. | Hugo Herbelin | |
| Note that localisation cannot be perfect anyways, as in the following example, where there is no way to highlight in the original input a syntactically stand-alone subterm where the error occurs. > Check forall (y:nat) (x:=0), y. > ^^^^^^^^^^^^^^^^^^^^^^^^ Error: In environment y : nat The term "let x := 0 in y" has type "nat" which should be Set, Prop or Type. | |||
| 2017-07-17 | Merge PR #781: Remove dead code [Universes.simplify_universe_context] | Maxime Dénès | |
| 2017-07-17 | Merge PR #783: Remove some useless code in Term_typing | Maxime Dénès | |
| 2017-07-17 | Merge PR #822: [meta] [api] Fix META file for API introduction. | Maxime Dénès | |
| 2017-07-17 | [funind] Remove spurious character in comment. | Emilio Jesus Gallego Arias | |
| It breaks ocamlmerlin. | |||
| 2017-07-17 | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | |
| 2017-07-17 | [meta] [api] Fix META file for API introduction. | Emilio Jesus Gallego Arias | |
| 2017-07-17 | Adding a coqdoc target to test-suite. | Hugo Herbelin | |
| One file was already ready for testing. We add another one. Note that we have to remove the machine-dependent lines in the output tex files. | |||
| 2017-07-17 | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | Maxime Dénès | |
| 2017-07-17 | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵ | Maxime Dénès | |
| moved to Global). | |||
| 2017-07-17 | Merge PR #879: Adding debug printers related to universes | Maxime Dénès | |
| 2017-07-17 | Merge PR #874: Adding econstr printer to "include" file. | Maxime Dénès | |
| 2017-07-17 | Merge PR #872: [travis] Display info on tested commit for PR builds. | Maxime Dénès | |
| 2017-07-17 | Merge PR #865: RefMan-ext: fix some typos | Maxime Dénès | |
| 2017-07-17 | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | Maxime Dénès | |
| rather than colors | |||
| 2017-07-17 | Merge PR #861: Fix typo in documentation for identity | Maxime Dénès | |
| 2017-07-16 | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | |
| Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo. | |||
| 2017-07-16 | Removing a dummy parameter in some FMapPositive statements. | Hugo Herbelin | |
| The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an unexpected extra dependency due to a name collision with a section variable. | |||
| 2017-07-16 | Adapting to 91df40272 (body_of_constant_body moved to global). | Hugo Herbelin | |
| 2017-07-15 | Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc). | Hugo Herbelin | |
| Fix proposed by the reporter, Vincent Laporte. Note that for LaTeX output, the selection of a keyword was already done after checking if the ident is recognized as a Coq ident by coqtop. Incidentally, being now explicit on an wildcard-catching of exceptions. | |||
| 2017-07-14 | Update with non structurally recursive | william-lawvere | |
| 2017-07-14 | Adding debug printers related to universes in the default debugger source file. | Pierre-Marie Pédrot | |
| 2017-07-14 | Fix a typo in dev/changes. | Pierre-Marie Pédrot | |
| 2017-07-14 | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | |
| 2017-07-14 | Getting rid of abstraction breaking code in tclABSTRACT. | Pierre-Marie Pédrot | |
| This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch. | |||
| 2017-07-13 | [travis] Update testing to 4.05.0 + Camlp5 7.01 | Emilio Jesus Gallego Arias | |
| 2017-07-13 | Removing a use of AUContext.instance in the STM. | Pierre-Marie Pédrot | |
| We only delay monomorphic proofs in quick mode, so that their universe context will always be empty. | |||
| 2017-07-13 | Removing the uses of abstraction-breaking code in Lemmas. | Pierre-Marie Pédrot | |
| I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints. | |||
| 2017-07-13 | Set version to 8.7+alpha. | Maxime Dénès | |
| It is a valid git tag (unlike 8.7~alpha) and will be considered by most tools as < 8.7.0 (unlike 8.7.0+alpha). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |