aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
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-18In recursive notations, accept partial application over the recursive pattern.Hugo Herbelin
This allows e.g. to support a notation of the form "x <== y <== z <= t" standing for "x <= y /\ y <= z /\ z <= t".
2020-11-17Merge PR #13390: Intern application arguments in left-to-right ordercoqbot-app[bot]
Reviewed-by: herbelin
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin
2020-11-17For printing, ordering notations by precision of the pattern.Hugo Herbelin
This relies on finer-than partial order check with. In particular: - number and order of notation metavariables does not matter - take care of recursive patterns inclusion
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-16Fixing alpha-equality of notation interpretations with recursive patterns.Hugo Herbelin
The name bound in binders were not checked up to alpha-equivalence, nor were the names binding the recursive patterns.
2020-11-16Using labels to document match_notation_constr.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
This allows to know which global references whose basename may be unexpectedly caught need to be qualified. Note: the alternative strategy, which is sometimes used, of renaming the binding variables so as to avoid collisions with the basename of a global reference is somehow less nice.
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-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
Fix #13249
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-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
This makes it so that we have an application `h a b` with both `a` and `b` unbound, `a` is the one that is reported (parent commit with my current compiler setup reports `b` first, and the code does not define which it should be). Ideally we would report both but that requires more code.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:41:09 +0000