aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-12Merge PR #12950: Notations: reworking the treatment of only-parsing and ↵coqbot-app[bot]
only-printing notations Reviewed-by: SkySkimmer
2020-10-10Adding change log for #12950.Hugo Herbelin
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.Hugo Herbelin
2020-10-10Adding a warning in case a notation is used neither for parsing nor printing.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
2020-10-10Splitting ssrbool's multi-printing notations into parsing and printing.Hugo Herbelin
This is in anticipation of a model with an explicit difference between a parsing-printing notation and the pair of only-parsing notation + only-printing notation.
2020-10-10Notation.ml: Move interpretation_eq earlier for future use.Hugo Herbelin
Also add optimisation of interpretation_eq.
2020-10-10Print Scope & cie: Add parentheses around notation interpretation.Hugo Herbelin
This is to be consistent with the use of parentheses in the syntax of Notation and to support a list of attribute afterwards.
2020-10-10Merge PR #13164: [bench] Dump the vo size difference.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
The current implementation of par: is still in the STM, but is optional. If the STM does not take over it, it defaults to the implementation of in comTactic which is based on all: (i.e. sequential). This commit also moved the interpretation of a tactic from g_ltac to vernac/comTactic which is more appropriate. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: silene
2020-10-09[bench] Dump the vo size difference.Pierre-Marie Pédrot
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
This fixes #12623 (bidirectionality breaks impredicativity).
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
Fix part of #8196, fix #12414 Replaces #9343
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-08Add a check of empty list of arguments in xmlprotocol where relevant.Hugo Herbelin
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a ↵coqbot-app[bot]
specific format. Reviewed-by: ejgallego
2020-10-08Merge PR #13159: update for Iris build system changescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-08update for Iris build system changesRalf Jung
2020-10-08Merge PR #13128: Define a new type instance_flag instead of using [unit option]Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13152: Algorithmically faster implementation of ↵coqbot-app[bot]
Evarconv.apply_on_subterm Reviewed-by: mattam82
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Explicitly pass around a state in Evarconv.second_order_matching.Pierre-Marie Pédrot
I know higher-order mutable state shared across call sites is a staple of Matthieu's style, but it is a footgun begging to be abused.
2020-10-07Algorithmically faster implementation of Evarconv.apply_on_subterm.Pierre-Marie Pédrot
Instead of repeatedly checking for evars to appear in a term, we perform the search in one single pass. This slowdown was observed in fiat-crypto. This is still a naive algorithm though, since we recompute the set of evars for each subterm. This is thus quadratic.
2020-10-06Merge PR #13141: Document the removal of forward class hints.coqbot-app[bot]
Reviewed-by: jfehrle Ack-by: ppedrot
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: Matafou Ack-by: ejgallego
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: Blaisorblade Ack-by: herbelin
2020-10-02More details in the documentation of native arraysVincent Semeria
Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Add persistent data structure Update doc/sphinx/language/core/primitive.rst Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-02Merge PR #13054: {new,setoid_}ring -> ringcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Fix retyping anomaly in rewriteGaëtan Gilbert
Fix #13045 Also make sure future anomalies won't be fed to tclzero. Instead of retyping with lax:true we may question why we produce an ill-typed term in decompose_app_rel: in the | App (f, [|arg|]) -> case we produce `fun x y : T => bla x y` but we have no assurance that the second argument of `bla` should have type `T`.
2020-09-30Merge PR #13021: Almost fully moving funind to new proof enginePierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:42:06 +0000