| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-22 | Ltac2 doc fix: syntax for extending an open variant type. | Théo Zimmermann | |
| 2019-05-22 | Use grep in changelog test instead of adhoc reads | Gaëtan Gilbert | |
| 2019-05-22 | Improve doc for generalizing binders | Gaëtan Gilbert | |
| 2019-05-22 | Merge PR #10207: Partly revert micromega parsing using typeclasses. | Vincent Laporte | |
| Reviewed-by: vbgl | |||
| 2019-05-22 | Fix #10208 don't fail when passed extensionless -topfile | Gaëtan Gilbert | |
| 2019-05-22 | Merge PR #9980: [ci] Set artifact expire date for all jobs. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-22 | Partly revert micromega parsing using typeclasses. | Frédéric Besson | |
| Typeclasses resolution is not used anymore for lia. Typeclasses resolution is still used by lra but only to access a database of declared constants. | |||
| 2019-05-22 | Update build-system.txt | Fourchaux | |
| 2019-05-21 | Fixing typos - Part 1 | JPR | |
| 2019-05-21 | [ci] Set artifact expire date for all jobs. | Emilio Jesus Gallego Arias | |
| Closes #8735 . | |||
| 2019-05-21 | Fixing a small bug in computing implicit arguments in (co-)fixpoints. | Hugo Herbelin | |
| The recursive functions and their binders were not pushed in the right order for implicit arguments. Additionally, we avoid calling push_name_env both for interpreting the type of each component of a (co-)fixpoint and for interpreting again the body of each component of a (co-)fixpoint because it may have side-effects (in the glob file). So we instead remember the part of its action on implicit arguments to replay it functionally. | |||
| 2019-05-21 | Adding test for old bug fixed in 8.5 (wrong implicit arguments in fixpoint). | Hugo Herbelin | |
| 2019-05-21 | Fixing an indentation in constrintern.ml. | Hugo Herbelin | |
| 2019-05-21 | [build] Select uint63 using `ocamlc -config` variables. | Emilio Jesus Gallego Arias | |
| This seems more robust and avoids having another implementation of `cp`. | |||
| 2019-05-21 | [loadpath] Factor in common logic for vio/vo file selection. | Emilio Jesus Gallego Arias | |
| 2019-05-21 | [loadpath] Further cleanup after merge with MlTop. | Emilio Jesus Gallego Arias | |
| We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged. | |||
| 2019-05-21 | [loadpath] Make loadpath handling self-contained and move to vernac | Emilio Jesus Gallego Arias | |
| We consolidate loadpath handling as a single `Loadpath` module from parts in `Library` and `Mltop`, placing it at the `vernac` level [as `Mltop`] This idea was first suggested in https://github.com/coq/coq/pull/9808 , and indeed it makes sense as library resolution tends to be business of the upper layers: IDE / build tools. Logic could be pushed upwards, but this is good enough for now. This consolidation has enabled some good and long overdue refactorings, and the module should become self-contained enough as to allow the resolution logic to be shared with `coqdep` in the future. The `Mltop` module only cares now about ML-level modules, and should go away once we rewrite the loader using `findlib` to solve https://github.com/coq/coq/issues/7698 . | |||
| 2019-05-21 | Merge PR #10188: Remove definition-not-visible warning | Emilio Jesus Gallego Arias | |
| Reviewed-by: gares | |||
| 2019-05-21 | Merge PR #10160: Miscellaneous fixes related to the command line | Vincent Laporte | |
| Ack-by: gares Ack-by: herbelin Reviewed-by: vbgl | |||
| 2019-05-21 | Overlay for definition-not-visible overhaul | Gaëtan Gilbert | |
| 2019-05-21 | Remove definition-not-visible warning | Gaëtan Gilbert | |
| This lets us avoid passing ~ontop to do_definition and co, and after #10050 to even more functions. | |||
| 2019-05-21 | Overlay for removing Instance: !type syntax | Gaëtan Gilbert | |
| 2019-05-21 | Remove undocumented Instance : ! syntax | Gaëtan Gilbert | |
| It's used a few times in the stdlib (a couple of which need no other change when removing the !) and not at all throughout our CI. Considering that I think it's fair enough to remove it. | |||
| 2019-05-21 | Merge PR #10042: [Classes] Use prepare_parameter from DeclareDef. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-21 | Merge PR #10174: Further cleanup of the side-effect machinery | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: maximedenes | |||
| 2019-05-21 | Merge PR #10144: Fix #9919: conversion functions are non-linear | Hugo Herbelin | |
| Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-05-20 | Minor Ltac2 documentation fix: type parameters are optional. | Théo Zimmermann | |
| 2019-05-20 | [Classes] Use prepare_parameter from DeclareDef. | Emilio Jesus Gallego Arias | |
| This code was originally part of #8811, authored by Gaëtan Gilbert. It seems we are not very consistent on what we do when we use `ParameterEntry`, specially w.r.t. universes but as code cleanup progresses we will have a better view. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2019-05-20 | Do not perform the section variable check on global recipes. | Pierre-Marie Pédrot | |
| By construction, we know that Cooking is returning the right set of used variables. This set has been checked already once at the time when the definition was performed inside the section. | |||
| 2019-05-20 | Ensure statically that declarations built by Term_typing are direct. | Pierre-Marie Pédrot | |
| This removes a lot of cruft breaking the opaque proof abstraction in Safe_typing and similar. | |||
| 2019-05-20 | Merge PR #9530: Remove `VtUnkown` classification | Gaëtan Gilbert | |
| Reviewed-by: JasonGross Reviewed-by: SkySkimmer | |||
| 2019-05-20 | Merge PR #10186: [CI/Azure/macOS] Target macOS version 10.11 | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-20 | Merge PR #9873: Remove test file with Timeout that failed spuriously. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-20 | Remove VtUnknown classification | Maxime Dénès | |
| This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. | |||
| 2019-05-20 | Remove Refine Instance Mode option | Maxime Dénès | |
| 2019-05-20 | Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax) | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-05-19 | [refman] Document etransitivity | Clément Pit-Claudel | |
| 2019-05-19 | [refman] Fix up the grammar entry for field_def | Clément Pit-Claudel | |
| 2019-05-19 | [refman] Add a .. cmd:: header for Reserved Notation and Reserved Infix | Clément Pit-Claudel | |
| Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | |||
| 2019-05-19 | [refman] Fix up the documentation of Instance and Existing Instance | Clément Pit-Claudel | |
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel | |
| 2019-05-19 | Merge PR #10184: A few nix-related updates | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-05-19 | Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ↵ | Théo Zimmermann | |
| notations Reviewed-by: Zimmi48 Ack-by: jfehrle | |||
| 2019-05-19 | Parameterize the constant_body type by opaque subproofs. | Pierre-Marie Pédrot | |
| 2019-05-19 | Make the type of constant bodies parametric on opaque proofs. | Pierre-Marie Pédrot | |
| 2019-05-19 | Merge the definition of constants and private constants in the API. | Pierre-Marie Pédrot | |
| 2019-05-19 | Inverting the responsibility to define logically a constant in Declare. | Pierre-Marie Pédrot | |
| The code was intricate due to the special handling of side-effects, while it was sufficient to extrude the logical definition to make it clearer. We thus declare a constant in two parts, first purely kernel-related, then purely libobject-related. | |||
| 2019-05-19 | Merge PR #10190: Implicit Quantifiers recurse in continuation of let-in | Hugo Herbelin | |
| Reviewed-by: herbelin | |||
| 2019-05-19 | Implicit Quantifiers recurse in continuation of let-in | Jasper Hugunin | |
| 2019-05-18 | Merge PR #10134: Simplify impargs | Hugo Herbelin | |
| Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: jashug | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |