aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
Reviewed-by: erikmd Reviewed-by: silene
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing ↵Pierre-Marie Pédrot
time and use location in some typing error messages Reviewed-by: ppedrot
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-12Merge PR #13156: Store the resolver of required modules as functor ↵coqbot-app[bot]
parameters in safe_env Reviewed-by: herbelin
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: MSoegtropIMC
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-12elpi 1.11.4Enrico Tassi
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
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-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were ↵Hugo Herbelin
missing.
2020-10-10Merge PR #13164: [bench] Dump the vo size difference.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-09Update pretyping/detyping.mlEnrico Tassi
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
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-09improve commentEnrico Tassi
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-09Store the resolver of required modules as functor parameters in safe_env.Pierre-Marie Pédrot
The safe environment features two different sets of delta resolvers, one for module parameters and one for the actual body of the module being built. The purpose of this separations seems to have been to reduce the number of name equations being added to the environment, since the one from the parameters would already be present at instanciation time. Semantically, required modules behave like parameters in this respect, i.e. delta resolvers that come from modules dependend upon are guaranteed to be added when that module is actually required. As such, there is no need to store the quotient coming from the dependencies inside the vo file of a given library. Yet, the previous code would precisely do that, leading to a potential quadratic blowup in vo file size, similarly to the issue with vio files storing the whole chain of dependency. This patch fixes the issue simply by segregating those redundant constraints in the dedicated field, thus dropping them from the vo.
2020-10-09[printing] make detyping resilient to "let x : _ := t in"Enrico Tassi
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 07:49:52 +0000