aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-03-21Merge PR #9789: [Manual] Improve documentation on Section, Variable, ContextThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: jfehrle
2019-03-21Merge PR #9695: [make install] Do not install the sphinx doctreesThéo Zimmermann
Reviewed-by: cpitclaudel Ack-by: ejgallego
2019-03-21Merge PR #9774: Remove clutter by moving historic unmaintained dev/doc files ↵Emilio Jesus Gallego Arias
to an archive subfolder. Reviewed-by: ejgallego
2019-03-20[coq] Adapt to coq/coq#9129 "removal of imperative proof state"Emilio Jesus Gallego Arias
2019-03-20Merge pull request coq/ltac2#113 from maximedenes/printed-by-envPierre-Marie Pédrot
Adapt to changes in Coq's printers API
2019-03-20Merge PR #9678: Stop accessing proof env via Pfedit in printersPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on ↵Gaëtan Gilbert
applications Reviewed-by: SkySkimmer
2019-03-20Fix CoqIDE progress bar.Pierre-Marie Pédrot
2019-03-20Add overlays for printer API changesMaxime Dénès
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
This should make https://github.com/coq/coq/pull/9129 easier.
2019-03-20Merge PR #9791: Fix constr_matching on SPropPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle
2019-03-20Merge PR #9746: Remove Term_typing.translate_mind indirectionEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-03-20Merge PR #9770: Correct dependencies in the micromega packEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-20Merge PR #9754: Don't lose the warning name when warning becomes error.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-20Merge PR #9805: [CI] Push the right commit to cachixEmilio Jesus Gallego Arias
2019-03-19[CI] Push the right commit to cachixVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 23:38:19 +0000