aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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)
2019-03-26Incorrect details in critical bug info (prop_set_proof_irrelevance)Gaëtan Gilbert
2019-03-26[kernel] Don't re-declare scheme side-effects that are already there.Emilio Jesus Gallego Arias
This is an experimental PR as I am not sure I can follow the reasoning in e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c Note that in safe_typing we avoid re-declaring effects twice. This removes a huge number of redeclaration of schemes side-effects that in fact are already generated such as `eq_ind`. Anyways we should deprecate the declaration of Schemes on-the-fly, I don't see the point honestly; just make sure your theory has the right ones. Well, going to a more eager declaration scheme could be costly in terms of size, so OMMV. TODO: only declare side-effects if the scheme is generated on-the-fly, add a parameter to the declaration function.
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-26Ignore generated files for CoqIDE bindingsVincent Laporte
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-26Fix syntax of Typeclasses eauto := in reference manual.Théo Zimmermann
2019-03-26Overlays for HoTT, Ltac2, and UniMathVincent Laporte
2019-03-26Declare initial hint databases in preludeMaxime Dénès
Previously, they were hard-wired in the ML code.
2019-03-26Fix for https://github.com/coq/coq/pull/8984Vincent Laporte
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 #9652: rewrite fails to detect lack of progressGaëtan Gilbert
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
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-21Merge PR #9797: [ci] Fix OCaml trunk build.Gaëtan Gilbert
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 10:21:33 +0000