aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-10Further cleanup: remove the local_reduction_function type.Pierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
This is extracted from #9710, where we need the environment anyway to compute iota rules on inductive types with let-bindings. The commit is self-contained, so I think it could go directly in to save me a few rebases. Furthermore, this is also related to #11707. Assuming we split cbn from the other reduction machine, this allows to merge the "local" machine with the general one, since after this PR they will have the same type. One less reduction machine should make people happy.
2020-05-10Merge PR #12235: Ensure eintros allows creating evarsKenji Maillard
Reviewed-by: kyoDralliam
2020-05-10Merge PR #12287: Define CRzero and CRone via CR_of_QMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-05-09Merge PR #12241: [declare] Merge DeclareDef into DeclareGaëtan Gilbert
Reviewed-by: Matafou Reviewed-by: SkySkimmer
2020-05-09Define CRzero and CRone via CR_of_QVincent Semeria
Add real numbers up to 10
2020-05-09Merge PR #12204: Ltac helper functions APIHugo Herbelin
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with ↵Hugo Herbelin
multiple scopes for the same inductive)
2020-05-09Merge PR #12040: Document the signing procedure of released binary packages.Maxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-05-08Merge PR #12272: Cleanup formatting in .. coqtop:: directivesClément Pit-Claudel
Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
Reviewed-by: pi8027 Reviewed-by: zeldovich
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12268: Add an example to motivate strictly positive occurrences checkThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
The API in `DeclareDef` should become the recommended API in `Declare`. This greatly reduces the exposure of internals; we still have a large offender in `Lemmas` but that will be taken care of in the next commit; effectively removing quite some chunks from `declare.mli`. This PR originally introduced a dependency cycle due to: - `Declare`: uses `Vernacexpr.decl_notation list` - `Vernacexpr`: uses `ComHint.hint_expr` - `ComHint`: uses `Declare.declare_constant` This is a real cycle in the sense that `ComHint` would have also move to `DeclareDef` in the medium term. There were quite a few ways to solve it, we have chosen to move the hints ast to `Vernacexpr` as it is not very invasive and seems consistent with the current style. Alternatives, which could be considered at a later stage are for example moving the notations AST to `Metasyntax`, having `Declare` not to depend on `Vernacexpr` [which seems actually a good thing to do in the medium term], reworking notation support more deeply...
2020-05-07[declare] Remove fix_exn internal access.Emilio Jesus Gallego Arias
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
Reviewed-by: Matafou Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2020-05-07Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Merge PR #12267: [ci] bump elpi to 1.11Emilio Jesus Gallego Arias
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-07Export API to recover values out of Ltac application.Pierre-Marie Pédrot
2020-05-07Add helper API to define low-level Ltac functions.Pierre-Marie Pédrot
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-06Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and ↵Hugo Herbelin
map_eq_app Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06Merge PR #12018: Adding properties about implb in Bool.vAnton Trunov
Ack-by: Blaisorblade Reviewed-by: anton-trunov
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Fix #12211Jason Gross
I forgot to test #12211 sufficiently; it was emitting timing info without saying which file was being timed, because the evaluation of `$@` was performed at the definition of `OCAMLC`. This fixes that issue of 8bd559370f51d7cc1877380a5ad726da67ceb0fa by delaying the evaluation of the definitions of `OCAMLC` and `OCAMLOPT` to the running of the recipies.
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
2020-05-05Merge PR #12252: [refman] Add missing (only parsing) to example of compat ↵Clément Pit-Claudel
notations.
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
There is no point in normalizing the goal in the legacy refiner because the function is actually insensitive to evars.
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-05[ssr] wrap a couple of exception with tclLIFTEnrico Tassi
2020-05-04[ssr] get rid of (pf_)mkSsrConstEnrico Tassi
2020-05-04Merge PR #12225: [ci] [doc] More detailed documentation for overlay buildingThéo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:24:14 +0000