aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Collapse)Author
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-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-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-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named ↵coqbot-app[bot]
variables. Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: SkySkimmer
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
This is a better abstraction barrier (no "symbol" type with uninterpreted ".." exported out of notation.ml). It also allows to "browse" notations mentioning a "..".
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
Fix #6042 Also introduce a deprecated compat option
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
Co-authored-by: <Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
We re-expose `declare_projections` and `declare_structure_entry` as it is needed by coq-elpi. Ideally we would provide a better way in recordops to interact with this, in fact `declare_structure_entry` is just a wrapper around recordops + libobject structure so there is hope it goes away entirely in the future. The need for Elpi to manually call `declare_projections` should actually disappear in future refactorings.
2020-11-13[record] Options API cleanup.Emilio Jesus Gallego Arias
2020-11-13[record] Refactor nested functions.Emilio Jesus Gallego Arias
In preparation for better handling of the regular record / class codepath. This will also allow to pack record data better.
2020-11-13[record] Cleanup of data structure and functions [2/2]Emilio Jesus Gallego Arias
In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here.
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here.
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
The IDENT annotations in g_ltac.mlg are required to not break the parser.
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
"Proof with" is Ltac-specific but there is no reason why it should be the same for "Proof using".
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ↵Pierre-Marie Pédrot
naming Ack-by: gares Reviewed-by: ppedrot
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next ↵coqbot-app[bot]
Obligation` Reviewed-by: SkySkimmer
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
Fixes #13320 . Trivial programming error, actually this is handled better in a further refactoring branch not submitted due to the long time the whole rework took.
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
Instead we store that data in the native code that was generated in adapt the compilation scheme accordingly. Less indirections and less imperative tinkering makes the code safer. The global symbol table was originally introduced in #10359 as a way not to depend on the Global module in the generated code. By storing all the native-related information in the cmxs file itself, this PR also makes other changes easier, such as e.g. #13287.
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ↵coqbot-app[bot]
a correct typing environment Reviewed-by: SkySkimmer
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
We accept patterns that we failed to type as a fallback.
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
Also some dead code. If no typo is introduced, there should be no semantic changes.
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
We reuse the standard code path for term interpretation instead of trying to mangle it.
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
The prepare_hint function was trying to requantify over all undefined evars, but actually this should not happen when defining generic terms as hints through some Hint vernacular command.
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02document Proof.compactEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Renaming Numeral into NumberPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-18 17:41:25 +0000