aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-01Merge PR #9872: Fix timing diff script to support non-utf8Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: jashug
2019-03-31Merge PR #9733: [lexer] keyword protected quotation token for arbitrary textPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-03-31Merge PR #8829: Error when [foo.(bar)] is used with nonprojection [bar], ↵Pierre-Marie Pédrot
warn if [bar] nonprimitive projection. Reviewed-by: ppedrot
2019-03-31Revert "iconv bedrock2 CI output to UTF-8"Jason Gross
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423. This commit is no longer necessary
2019-03-31[pretty-timing scripts] Don't barf on non-utf-8Jason Gross
This fixes #9767 by silently ignoring input lines which are not valid UTF-8. We hereby assume that all file paths are valid UTF-8. We also now actually test both python2 and python3 on the CI.
2019-03-31[pretty-print py]Don't print sys.stdout;better utfJason Gross
This should fix #9705 I'm kind-of cargo-cult coding here, from things like https://docs.python.org/3/library/sys.html#sys.displayhook and https://github.com/coq/coq/issues/9705#issuecomment-471996313, but hopefully this fixes the issue without breaking anything. (I am really a novice when it comes to the str/bytes distinction in python3.)
2019-03-31documentationEnrico Tassi
2019-03-31overlay for ltac2Enrico Tassi
2019-03-31[parsing] add keyword-protected generic quotationEnrico Tassi
One can now register a quotation using a grammar rule with QUOTATION("name:"). "name:" becomes a keyword and the token is generated for name: followed by a an identifier or a parenthesized text. Eg constr:x string:[....] ltac:(....) ltac:{....} The delimiter is made of 1 or more occurrences of the same parenthesis, eg ((.....)) or [[[[....]]]]. The idea being that if the text happens to contain the closing delimiter, one can make the delimiter longer and avoid confusion (no escaping). Eg string:[[ .. ']' .. ]] Nesting the delimiter is allowed, eg ((..((...))..)) is OK. The text inside the quotation is returned as a string (including the parentheses), so that a third party parser can take care of it. Keywords don't need to end in ':'.
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
Tokens were having a double role: - the output of the lexer - the items of grammar entries, especially terminals Now tokens are the output of the lexer, and this paves the way for using a richer data type, eg including Loc.t Patterns, as in Plexing.pattern, only represent patterns (for tokens) and now have a bit more structure (eg the wildcard is represented as None, not as "", while a regular pattern for "x" as Some "x")
2019-03-31[dune] typoEnrico Tassi
2019-03-31Merge PR #9841: Remove some [let foo = foo] in eqschemesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp ↵Pierre-Marie Pédrot
skip_pattern Reviewed-by: ppedrot
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
2019-03-30Merge PR #8730: Add unicode category LMPierre-Marie Pédrot
Reviewed-by: jashug Ack-by: ppedrot Reviewed-by: vbgl
2019-03-30Merge PR #9869: [CI] Force caching when running test-suite in async modeEmilio Jesus Gallego Arias
2019-03-29Merge PR #9858: Fix top_printers after removal of imperative stateEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-29Merge PR #9830: [parser] initialization based on Loc.t rather than Loc.sourceEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: gares
2019-03-29[CI] Force caching when running test-suite in async modeMaxime Dénès
I thought the test-suite infrastructure was always passing `-async-proofs-cache force`, but in fact it does it only for interactive tests. This should speed up the tests quite a bit.
2019-03-29Merge PR #9866: typo in ring.rstThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9860: [dune] Fix shim quoting and add coqc wrapper.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9859: [dune] Don't regenerate ltac/dune after bootstrapping.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9853: Use only lowercase for unimath in CI scriptsEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-03-29typo in ring.rstthery
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
In this way one can also set the current offsets in a file, useful if you are parsing a Coq fragment within a file instead of a full file starting from the first line.
2019-03-29Merge PR #9834: Ignore generated files for CoqIDE bindingsGaëtan Gilbert
Reviewed-by: gares
2019-03-28[dune] Fix shim quoting and add coqc wrapper.Emilio Jesus Gallego Arias
The quoting was incorrect thus scripts didn't properly work.
2019-03-28[dune] Don't regenerate ltac/dune after bootstrapping.Emilio Jesus Gallego Arias
Once we have the good `plugins/ltac/dune` in place for bootstrapping, we should not regenerate it. Thanks to @maximedenes for the report. This fixes `make states` always rebuilding ltac's dependencies.
2019-03-28Fix top_printers after removal of imperative stateGaëtan Gilbert
There's never a proof available in ocamldebug I don't know about Drop.
2019-03-28Use only lowercase for unimath in CI scriptsGaëtan Gilbert
Fix #9845
2019-03-28Merge PR #9129: [proof] Removal of imperative state ; interpretation layers ↵Maxime Dénès
only. Ack-by: SkySkimmer Reviewed-by: aspiwack Ack-by: ejgallego Ack-by: gares Ack-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027
2019-03-28Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-27Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.Jim Fehrle
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
This is convenient for the bootstrap of `coqdep`
2019-03-27[doc] [abstract] Document a bit some problems with abstract.Emilio Jesus Gallego Arias
2019-03-27[funind] Try to be more precise with universe contexts in recdef hooks.Emilio Jesus Gallego Arias
2019-03-27[proof_global] [ci] Overlays for removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
We try to do a bit of cleanup for the `with_fail` function, this still is delicate code.
2019-03-27[vernac] Thread proof state to declare_assumption for warningEmilio Jesus Gallego Arias
Not sure the warning is worth the extra parameter.
2019-03-27[vernacular] Make `Show` fail again when no goals remain.Emilio Jesus Gallego Arias
This is used in the test-suite to check that a proof is closed; I am not sure we'd like to keep this patch tho: the non-failing semantics seems saner for IDEs. [main users are in `test-suite/ide`]
2019-03-27[vernac] Allow path for `save_proof` where no proof state is present.Emilio Jesus Gallego Arias
In that case the terminator and proof object have to be supplied in the ?proof argument, or else we get an anomaly. Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
2019-03-27[plugin tutorial] Adapt to removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [funind] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [derive] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [setoid_ring] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [micromega] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [ssr] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:54:31 +0000