aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-22[Ltac2] Add util files for Bool, List, OptionJason Gross
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-22Merge PR #10211: Use grep in changelog test instead of adhoc readsThéo Zimmermann
2019-05-22Merge PR #10203: Fixing typos - Part 1Théo Zimmermann
2019-05-22Merge PR #10178: Improve doc for generalizing bindersThéo Zimmermann
2019-05-22Use grep in changelog test instead of adhoc readsGaëtan Gilbert
2019-05-22Improve doc for generalizing bindersGaëtan Gilbert
2019-05-22Merge PR #10207: Partly revert micromega parsing using typeclasses.Vincent Laporte
2019-05-22Merge PR #9980: [ci] Set artifact expire date for all jobs.Gaëtan Gilbert
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2019-05-21[ci] Set artifact expire date for all jobs.Emilio Jesus Gallego Arias
2019-05-21Merge PR #10188: Remove definition-not-visible warningEmilio Jesus Gallego Arias
2019-05-21Merge PR #10160: Miscellaneous fixes related to the command lineVincent Laporte
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Merge PR #10042: [Classes] Use prepare_parameter from DeclareDef.Gaëtan Gilbert
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-20[Classes] Use prepare_parameter from DeclareDef.Emilio Jesus Gallego Arias
2019-05-20Do not perform the section variable check on global recipes.Pierre-Marie Pédrot
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-20Merge PR #9530: Remove `VtUnkown` classificationGaëtan Gilbert
2019-05-20Merge PR #10186: [CI/Azure/macOS] Target macOS version 10.11Gaëtan Gilbert
2019-05-20Merge PR #9873: Remove test file with Timeout that failed spuriously.Gaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-20Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax)Théo Zimmermann
2019-05-19[refman] Document etransitivityClément Pit-Claudel
2019-05-19[refman] Fix up the grammar entry for field_defClément Pit-Claudel
2019-05-19[refman] Add a .. cmd:: header for Reserved Notation and Reserved InfixClément Pit-Claudel
2019-05-19[refman] Fix up the documentation of Instance and Existing InstanceClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10184: A few nix-related updatesThéo Zimmermann
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...Théo Zimmermann
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-19Inverting the responsibility to define logically a constant in Declare.Pierre-Marie Pédrot
2019-05-19Merge PR #10190: Implicit Quantifiers recurse in continuation of let-inHugo Herbelin
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-18Merge PR #10134: Simplify impargsHugo Herbelin
2019-05-17[CI/Azure/macOS] Target macOS version 10.11Vincent Laporte
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[default.nix] Exclude the nix/ directory from sourcesVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:31:30 +0000