| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-20 | Enforcing when a binding variable has no explicit type in constr_notation. | Hugo Herbelin | |
| This avoids relying on fragile invariants. | |||
| 2020-11-20 | A step towards supporting pattern cast deeplier. | Hugo Herbelin | |
| We at least support a cast at the top of patterns in notations. | |||
| 2020-11-20 | Add preliminary support for notations with large class (non-recursive) binders. | Hugo Herbelin | |
| We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat". | |||
| 2020-11-20 | Rewriting convoluted code of set_var_scope in constrintern.ml. | Hugo Herbelin | |
| 2020-11-20 | Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions ↵ | coqbot-app[bot] | |
| between variable and non-qualified global references Reviewed-by: ejgallego Ack-by: maximedenes Ack-by: gares | |||
| 2020-11-20 | Merge PR #13360: Fix incorrect name refreshing when interning a generalized ↵ | coqbot-app[bot] | |
| binder Reviewed-by: herbelin | |||
| 2020-11-19 | Merge 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-18 | In 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-17 | Merge PR #13390: Intern application arguments in left-to-right order | coqbot-app[bot] | |
| Reviewed-by: herbelin | |||
| 2020-11-17 | A reimport of notations now put the corresponding notations again in front. | Hugo Herbelin | |
| 2020-11-17 | For 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-17 | Merge PR #12653: Syntax for specifying cumulative inductives | coqbot-app[bot] | |
| Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot | |||
| 2020-11-16 | Fixing 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-16 | Using labels to document match_notation_constr. | Hugo Herbelin | |
| 2020-11-16 | Fix #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-16 | Merge 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-16 | Fix incorrect name refreshing when interning a generalized binder | Gaëtan Gilbert | |
| Fix #13249 | |||
| 2020-11-16 | Merge PR #12685: Propagating scope information in indirect application to a ↵ | Pierre-Marie Pédrot | |
| reference. Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2020-11-16 | Syntax for specifying cumulative inductives | Gaëtan Gilbert | |
| 2020-11-15 | Intern application arguments in left-to-right order | Gaë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-15 | Adding support for Locate "( x , y )". | Hugo Herbelin | |
| It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-11-15 | Fixing 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-15 | Moving 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-15 | Indentation. | Hugo Herbelin | |
| 2020-11-15 | Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly. | Hugo Herbelin | |
| 2020-11-15 | Propagating 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-12 | Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop | coqbot-app[bot] | |
| Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego | |||
| 2020-11-12 | Change Dumpglob.pause and Dumpglob.continue into push and pop | Lasse Blaauwbroek | |
| Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-11-12 | Merge 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-06 | Merge PR #13255: Fixes #13244: support for coercions in Search | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2020-11-05 | Minor cut elimination in the code of constrintern.ml. | Hugo Herbelin | |
| 2020-11-05 | Accept local variables in mixed terms and binders of notations. | Hugo Herbelin | |
| 2020-11-05 | Accept section variables in notations with mixed terms and binders. | Hugo Herbelin | |
| 2020-11-05 | Passing 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-05 | Notations: 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-05 | Merge PR #12218: Numeral notations for non inductive types | coqbot-app[bot] | |
| Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48 | |||
| 2020-11-05 | Rename Dec and HexDec to Decimal and Hexadecimal | Pierre Roux | |
| As noted by Hugo Herbelin, Dec is rather used for "decidable". | |||
| 2020-11-05 | Allow multiple primitive notation on the same scope and triggers | Pierre 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 inductives | Pierre Roux | |
| 2020-11-05 | [numeral notation] Add support for parameterized inductives | Pierre Roux | |
| 2020-11-05 | [numeral notation] Allow to put/ignore holes during pre/postprocessing | Pierre 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/postprocessing | Pierre 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-04 | Add functions Smartlocate.global_{constant,constructor} | Pierre Roux | |
| 2020-11-04 | Typing patterns and using type constraints in Search. | Hugo Herbelin | |
| We accept patterns that we failed to type as a fallback. | |||
| 2020-11-04 | Adding a typed interpretation of patterns. | Hugo Herbelin | |
| 2020-11-04 | Factorizing 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-04 | Moving interpretation of user-level universes in constrintern.ml. | Hugo Herbelin | |
| 2020-11-03 | Merge PR #13132: Understand Mangle Names in implicit generalization | coqbot-app[bot] | |
| Reviewed-by: herbelin | |||
| 2020-11-03 | Merge 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-30 | Renaming Numeral into Number | Pierre Roux | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |