aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in extended-pattern-matching.rstGaëtan Gilbert
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
2019-02-12Fix doc for coqtop:: undoGaëtan Gilbert
2019-02-12Increase sphinx recursion limitGaëtan Gilbert
Not sure why but it seems required for future commits.
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-11Don't save expected failure logs from opened/ bugs.Gaëtan Gilbert
Grepping for "Error!" is how we decide if we exit with failure or not. I don't remember why I used the "==> FAILURE <==" string in the save-logs script but it was an error.
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-11[ide] fix unconditional goto-point on editing an error (fix #9488)Enrico Tassi
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-11Fix #9508: Unexpected interaction between implicit arguments and primitive ↵Pierre-Marie Pédrot
projections. This was due to an involuntary capture of a variable name.
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-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
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[coqdoc] Add the From keywordPierre Roux
2019-02-11Use math mode more.Tanaka Akira
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf. And two "x:T" are quoted.
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
Use LEFT DOUBLE QUOTATION MARK (U+201C) and RIGHT DOUBLE QUOTATION MARK (U+201D) instead of QUOTATION MARK (U+0022). QUOTATION MARK is formatted as same form both for opening and closing quotation mark.
2019-02-11Remove a space before closing double-quote.Tanaka Akira
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-10Change "I" to "I_p".Tanaka Akira
Since the type of "c" is "I_p ...", the constructor should return the value of it.
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
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[coq] Adapt to coq/coq#9137Emilio Jesus Gallego Arias
To be merged when the upstream PR is merged. Not sure this is the right thing to do tho.
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-09Merge pull request coq/ltac2#102 from maximedenes/rm-unknownPierre-Marie Pédrot
Remove VtUnknown classification
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 21:12:33 +0000