aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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)
2019-03-26Incorrect details in critical bug info (prop_set_proof_irrelevance)Gaëtan Gilbert
2019-03-26Fix make sphinx failureJim Fehrle
2019-03-26Merge PR #9690: Fix 9663 (Miller pattern unification fails on evars)Matthieu Sozeau
Ack-by: ggonthier Reviewed-by: mattam82
2019-03-26Merge PR #9833: Improve the backport script.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-26Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elimMaxime Dénès
Ack-by: gares Ack-by: maximedenes
2019-03-26[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)Enrico Tassi
In particular evar_eqappr_x tries to find a miller pattern on both sides, while the fast path for evars tries solve_simple_eqn in one direction only. So if you have (Evar-not-miller = Evar-miller) the code was not trying to solve the RHS.
2019-03-26Improve the backport script.Guillaume Melquiond
It now uses the origin/master branch rather than the master branch, thus avoiding the need for local merges. More importantly, it no longer creates a subshell in case of conflicts, but instead gives control back to the user. Once conflicts are solved, it suffices to relaunch the script (instead of exiting the subshell). The reason is that, otherwise, there was no sane way of giving up a backport, due to the infinite subshell loop.
2019-03-26Merge PR #9826: [ssr] Two small improvementsEnrico Tassi
Reviewed-by: gares
2019-03-26Merge PR #9829: [Vernacular] Deprecate the “Show Script” commandEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares # Conflicts: # CHANGES.md
2019-03-25Merge PR #8094: Remove `Automatic Coercions Import` option.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
Fixes #8320
2019-03-25Move code ownership of reals library to new maintainer team.Théo Zimmermann
2019-03-25[ssr] Use Coqlib in “abstract”Vincent Laporte
2019-03-25[ssr] More detailed error message in rewriteVincent Laporte
2019-03-25[ssr] avoid HO unif when doing truncation analysisEnrico Tassi
Eliminators can be: - dependent: ... -> forall x (y : I x), P x y - truncated: ... -> forall x (y : I x), P x - funind like: ..-> forall x, P t The user may provide a term t in `elim: t` - t may be the last argument - t may be the last "pattern" (standing for the last argument of P) We use unification to see if t (and its type) fits in one of these cases (and/or to infer t). This patch refuses to use unification in the HO case eg `?T a = t` since the result is too often a false positive.
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
This option made the Coercions command follow non-standard scoping rules (effect on `Require` rather than `Import`). It was already marked for deletion in 8.8.
2019-03-25Merge PR #9823: Fix typoThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-03-25Merge PR #9586: Use named_context_val for fast lookup in intern named referenceEmilio Jesus Gallego Arias
Reviewed-by: herbelin Reviewed-by: ppedrot
2019-03-25Fix indentationGan Shen
2019-03-25Update doc/sphinx/language/gallina-extensions.rstThéo Zimmermann
Co-Authored-By: gshen42 <gan.shen@outlook.com>
2019-03-24Fix typoGan Shen
2019-03-23Merge PR #9822: [ci] [gitlab] Pin ocamlfind to masterGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-23[ci] [gitlab] Pin ocamlfind to masterEmilio Jesus Gallego Arias
https://gitlab.camlcity.org/gerd/lib-findlib/merge_requests/22 was merged, so we may indeed pin to the main dev repos until a new findlib is released.
2019-03-22Merge PR #8560: Unicode bindings for CoqIDE that works out of the boxPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: charguer Reviewed-by: gares Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:25:52 +0000