aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
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 #12685: Propagating scope information in indirect application to a ↵Pierre-Marie Pédrot
reference. Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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-15Indentation.Hugo Herbelin
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
This allows the following to interpret "0" in the expected scope: Notation "0" := true : bool_scope. Axiom f : bool -> bool -> nat. Record R := { p : bool -> nat }. Check (@f 0) 0. Check fun r => r.(@p) 0.
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Passing full interning env to pattern interning, for better control.Hugo Herbelin
This will allow for instance to check the status of a variable name used both as a term and binder in notations.
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
Currently, global references in patterns used also as terms were accepted for parsing but not for printing. We accept section variables for both parsing and printing. We reject constant and inductive types for both parsing and printing. Among other, this also fixes a hole in interpreting variables used both patterns and terms: the term part was not interpreted.
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-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
Until now, declaring a number or string notation on some trigger removed all previous notations on the same scope. Bug discovered by Jason Gross while reviewing #12218.
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Allow to put/ignore holes during pre/postprocessingPierre Roux
This will enable to handle implicit arguments by ignoring them during preprocessing (before uninterpreting (i.e., printing)) and remplace them with holes `_` during postprocessing (after interpreting (i.e., parsing)).
2020-11-04[numeral notation] Add a pre/postprocessingPierre Roux
This will enable to define numeral notation on non inductive by using an inductive type as proxy and those translations to translate to/from the actual type to the inductive type.
2020-11-04Add functions Smartlocate.global_{constant,constructor}Pierre Roux
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-04Adding a typed interpretation of patterns.Hugo Herbelin
2020-11-04Factorizing UState.make* through UState.from_env, to highlight the similarity.Hugo Herbelin
An alternative could also be to split the initialization of the environment and the declaration of initial "binders".
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
Reviewed-by: herbelin
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-10-30Renaming Numeral into NumberPierre Roux
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
This is similar to Constant and MutInd but for some reason this was was never done. Such a patch makes the whole API more regular. We also deprecate the legacy aliases.
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation.
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
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-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.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-10Notation.ml: Move interpretation_eq earlier for future use.Hugo Herbelin
Also add optimisation of interpretation_eq.
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-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
Fix #13117 We alternatively could fix the generation of the data with Existing Class but I prefer moving towards removing it.
2020-10-06Simplify Implicit_quantifiers.combine_params a bitGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaëtan Gilbert
Used only by implicit_quantifiers
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:59:47 +0000