aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-13more testsEnrico Tassi
2019-02-13refactor grammarEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
(when defining a new constant)
2019-02-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-13Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: mattam82 Ack-by: maximedenes Reviewed-by: ppedrot
2019-02-12Merge PR #9548: Almost fully type-safe gramlib implementationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-12Merge PR #9563: Improve the documentation of auto.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2019-02-12Improve the documentation of auto.Théo Zimmermann
In particular, mention that auto does not use full-blown apply.
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary.
2019-02-11Merge PR #9551: Small typos in the documentation.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
Reviewed-by: CohenCyril Fixes a bug introduced by PR #9341
2019-02-11[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
This is the completion of #9070, needed in order to serialize ssreflect programs properly. TTBOK this completes the interface for all generic arguments.
2019-02-11Merge PR #9544: [coqargs] Minor refactoring of error functions.Enrico Tassi
Reviewed-by: gares
2019-02-11Merge PR #9531: [test-suite] Improve test for async workers.Enrico Tassi
Reviewed-by: gares
2019-02-11Small typos in the documentation.Martin Bodin
2019-02-11Almost fully type-safe implementation of camlp5.Pierre-Marie Pédrot
There are still minute uses of type-unsafe primitives. Most of them can be removed if I had a little higher dan in GADTs (or weeks to spare thinking about how non-interactive proofs can be performed) but one, which is really a potential source of unsoundness. The latter is not problematic as all uses in Coq are protected about the unsoundness proof, but the API is clearly deficient and needs to be fixed at some point.
2019-02-11Further propagation of well-typedness in Grammar.Pierre-Marie Pédrot
2019-02-11Introduce a GADT of well-typed grammar entries in Grammar.Pierre-Marie Pédrot
Not fully used yet, we rely on erasure casts for now.
2019-02-11Centralizing the calls to the global mutable grammar in Grammar.Pierre-Marie Pédrot
2019-02-11Specialize the intermediate types of the Grammar functor.Pierre-Marie Pédrot
Now that we depend on a module argument, we do not have to quantify over the arguments anymore.
2019-02-11Make Grammar truly functorial.Pierre-Marie Pédrot
The old implementation was simply hiding the fact that the functor relied on a generic data type. If we want to implement the grammar engine in a truly type-safe way, we need to make the ancilliary datatypes depend on the type parameters.
2019-02-11Move most of Gramext into Grammar.Pierre-Marie Pédrot
This module was defining unsafe functions and datatypes only relevant to the grammar engine. We hide them under the API so as to be able to later clean it up.
2019-02-11Merge PR #9465: [Nix-CI] Add iris and lambda-rustMaxime Dénès
Reviewed-by: maximedenes
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
We remove a few ad-hoc `exit` from the code as error handling really ought to be centralized.
2019-02-11Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-11Merge PR #9543: [ocamldebug] Fix load order after gramlib refactoring.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-11Merge PR #9522: Update link to refman for master branch.Vincent Laporte
Reviewed-by: vbgl
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-11[ocamldebug] Fix load order after gramlib refactoring.Emilio Jesus Gallego Arias
2019-02-11Merge PR #9478: Remove the comment fields of locations.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-11Merge PR #9534: Workaround for CI not having enough RAM for bedrock2: ↵Emilio Jesus Gallego Arias
`-async-proofs-tac-j 1` Reviewed-by: ejgallego
2019-02-10Merge PR #9535: [readme] Add link to information about release plans.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-02-10Merge PR #9536: [ci] Remove unused bintray file.Maxime Dénès
Reviewed-by: maximedenes
2019-02-09remove `allow_failure: true` for bedrock2Samuel Gruetter
2019-02-09remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed ↵Samuel Gruetter
passed https://gitlab.com/coq/coq/-/jobs/158737429
2019-02-09Update link to refman and stdlib doc for master branch.Théo Zimmermann
2019-02-09[ci] Remove unused bintray file.Emilio Jesus Gallego Arias
Not needed anymore after Travis was removed.
2019-02-09[readme] Add link to information about release plans.Emilio Jesus Gallego Arias
This is a proposal to use the wiki to gather current information about the release process.
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile, and we use VERBOSE=1 for better debuggability
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-02-08[test-suite] Improve test for async workers.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
Reviewed-by: gares
2019-02-08Merge PR #9492: [stm] Filter some more arguments that shouldn't be sent to ↵Enrico Tassi
workers. Reviewed-by: gares
2019-02-08Merge PR #9504: Add print_pure_econstr signatureGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in ↵Théo Zimmermann
Docker Hub Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 02:48:34 +0000