aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
This avoids relying on fragile invariants.
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
We at least support a cast at the top of patterns in notations.
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-11-20Rewriting convoluted code of set_var_scope in constrintern.ml.Hugo Herbelin
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions ↵coqbot-app[bot]
between variable and non-qualified global references Reviewed-by: ejgallego Ack-by: maximedenes Ack-by: gares
2020-11-20Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof informationcoqbot-app[bot]
Reviewed-by: gares
2020-11-20Merge PR #13426: [doc] [ssr] fix documentation of reflectcoqbot-app[bot]
Reviewed-by: CohenCyril
2020-11-20Merge PR #13399: Miscellaneous ring improvements in code + error messagesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically ↵Pierre-Marie Pédrot
an arity. Reviewed-by: ppedrot
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized ↵coqbot-app[bot]
binder Reviewed-by: herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-20Update ↵Hugo Herbelin
doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a ↵coqbot-app[bot]
primitive projection was wrongly supposed to be already inferred Reviewed-by: gares
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to ↵coqbot-app[bot]
template poly Reviewed-by: gares Reviewed-by: herbelin
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
After the previous commit, the stm should correctly pass proof information, thus we make `proof_object` carry it removing a bunch of internal code.
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
Since 8.5, the STM could not delegate proof information it was contained inside a closure. This could potentially create some problems, as witnessed in #12586. Recent refactoring have reified however much of this state, so it seems a good idea to use bits of the state now, at the cost of introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of ↵coqbot-app[bot]
debug / info_eauto. Reviewed-by: jfehrle
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
This is to make more explicit that arguments of the projection are not kept. We seize this opportunity to use QGlobRef equality on GlobRef.
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown ↵Hugo Herbelin
type. This was a case where expand_projections was calling find_mrectype which was expecting the argument of the projection to be an inductive. We could have ensured that this type is at least the appropriate inductive applied to fresh evars, but this expand_projections was in practice used for checking the applicability of canonical structures and the unifiability of the parameters of the projections is anyway a consequence of the unifiability of the principal argument of the projections. So, the latter is enough.
2020-11-19Merge PR #13421: Fix typo in rst link syntax.coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
2020-11-19Merge PR #12959: Improve the bytecode interpreterPierre-Marie Pédrot
Ack-by: ppedrot Reviewed-by: proux01
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ↵coqbot-app[bot]
then by last imported Reviewed-by: Zimmi48 Ack-by: RalfJung Ack-by: gares
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares
2020-11-18Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Merge PR #13410: [configure] check that zarith dev files are availablecoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: silene
2020-11-18[configure] check that zarith dev files are availableEnrico Tassi
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-18[attributes] Add overlays for #13312Emilio Jesus Gallego Arias
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-18Merge PR #13400: [doc] add a link to v8.13coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-18Add more explicit tests for next_up and next_down.Pierre Roux
2020-11-18[attributes] Allow boolean, single-value attributes.Emilio Jesus Gallego Arias
Following discussion in https://github.com/coq/coq/pull/12586 , we extend the syntax `val=string` to support also arbitrary values. In particular we support boolean ones, or arbitrary key-pair lists. This complements the current form `val="string"`, and makes more sense in general. Current syntax for the boolean version is `attr=yes` or `attr=no`, but we could be more liberal if desired. The general new guideline is that `foo(vals)` is reserved for the case where `vals` is a list, whereas `foo=val` is for attributes that allow a unique assignment. This commit only introduces the support, next commits will migrate some attributes to this new syntax and deprecate the old versions.
2020-11-18Merge PR #13220: Give a typical example of Makefile wrapper for coq_makefile ↵coqbot-app[bot]
(addresses #12903) Reviewed-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-11-18Merge PR #12765: In recursive notations, accept partial application over the ↵coqbot-app[bot]
recursive pattern Reviewed-by: gares Ack-by: maximedenes Ack-by: jfehrle
2020-11-18Merge PR #13341: Finish fixing setoid rewrite under anonymous lambdas ↵Pierre-Marie Pédrot
(hopefully) Reviewed-by: ppedrot
2020-11-18Merge PR #13251: Make sure that setoid_rewrite passes state to subgoalsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-18Update doc/sphinx/practical-tools/utilities.rstHugo Herbelin
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 04:58:53 +0000