aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-29[dune] Full Dune support.Emilio Jesus Gallego Arias
This add experimental support for building the full Ltac2 plugin with Dune, see tree at https://github.com/ejgallego/dune/tree/coq
2019-03-29Merge PR #9834: Ignore generated files for CoqIDE bindingsGaëtan Gilbert
Reviewed-by: gares
2019-03-28Merge pull request coq/ltac2#109 from ejgallego/proof+no_global_partialPierre-Marie Pédrot
[coq] Adapt to coq/coq#9129 "removal of imperative proof state"
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
2019-03-27Merge PR #9819: Fix make sphinx failure on WindowsEnrico Tassi
Reviewed-by: gares
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
This is in view of the 8.10 release, after which we will remove the option and the `VtUnknown` classification.
2019-03-27[nix] Update reference to nixpkgsVincent Laporte
2019-03-27Merge PR #9837: Fix some critical-bugs informationsThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-26Fix reproduction info for some past critical bugsGaëtan Gilbert
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v - test-suite/failure/inductive4.v is now .../inductive.v - repro for #4157 now added to the repo (it was in an unmerged commit on @herbelin's repo) - commit message of 244d7a9aa contains a repro for its bug (I didn't bother adding to the test suite as a return of the bug could just as well use different strings so the specific repro wouldn't test anything useful)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 18:27:41 +0000