aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
We add state handling to tactics. TODO: - [rewrite] `add_morphism_infer` creates problems as it opens a proof. - [g_obligations] with_tac
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[tactic] Adapt tactic layer to removal of imperative proof state.Emilio Jesus Gallego Arias
State in `Proof_global` was mostly used for debugging, so not a big change.
2019-03-27[printing] Removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[proof_global] Removal of imperative state.Emilio Jesus Gallego Arias
We change the API; after some thinking the tradeoff is clear in favor of the more radical functional option from the start. We also guarante the existence of a proof is by typing now, so exceptions `NoCurrentProof` and `NoSuchGoal` are gone. TODO: Review what's going on with focusing now.
2019-03-27Merge PR #9827: Move code ownership of reals library to new maintainer team.Maxime Dénès
Reviewed-by: maximedenes
2019-03-27Remove some [let foo = foo] in eqschemesGaëtan Gilbert
2019-03-27Merge PR #9807: Fix CoqIDE progress bar.Enrico Tassi
Reviewed-by: Zimmi48
2019-03-27Merge PR #9825: Deprecate `Refine Instance Mode` optionThéo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:06:37 +0000