| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-07 | [abbreviation] allow the user to set arguments scope | Enrico Tassi | |
| 2021-04-07 | cleanup: remove confusing sharing | Enrico Tassi | |
| 2021-04-07 | cleanup: less exceptions, removal of try_interp_name_alias | Enrico Tassi | |
| 2021-03-26 | [recordops] complete API rewrite; the module is now called [structures] | Enrico Tassi | |
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
| 2020-12-11 | Removing non relevant argument binding_kind of GLocalDef. | Hugo Herbelin | |
| 2020-12-09 | Using self-documenting argument names in two exceptions of cases.ml. | Hugo Herbelin | |
| Namely, WrongNumargInductive and WrongNumargConstructor. | |||
| 2020-12-09 | Constrintern.ml: some naming uniformity. | Hugo Herbelin | |
| 2020-12-09 | Some documentation in constrintern.ml. | Hugo Herbelin | |
| 2020-12-09 | Fixing some indentations in constrintern.ml. | Hugo Herbelin | |
| Also includes a try/let commutation for uniformity. | |||
| 2020-12-09 | Constrintern: Code factorization in interning of record fields. | Hugo Herbelin | |
| Also includes some fine-tuning of error messages. | |||
| 2020-12-09 | Constrintern: Grouping together functions about reference locating. | Hugo Herbelin | |
| 2020-12-09 | Constrintern cleanup: Centralizing calls to find_appl_head. | Hugo Herbelin | |
| There are calls now in intern_impargs and CAppExpl. This seems clearer and eventually allow to factorize code between term and pattern interning. | |||
| 2020-12-09 | Fixing support for argument scopes and let-ins while interning cases patterns. | Hugo Herbelin | |
| We also simplify the whole process of interpretation of cases pattern on the way. | |||
| 2020-12-09 | Move addition of parameters in asymmetric mode to first phase of pat interning. | Hugo Herbelin | |
| 2020-12-09 | Removing a useless explicit use of subscopes in interpreting arguments of a ↵ | Hugo Herbelin | |
| notation. | |||
| 2020-12-09 | Constrintern: As in terms, accept @C for C abbreviation in cases patterns. | Hugo Herbelin | |
| 2020-12-09 | Constrintern: shortcut in cases pattern interning. | Hugo Herbelin | |
| 2020-11-25 | Separate interning and pretyping of universes | Gaëtan Gilbert | |
| This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern. | |||
| 2020-11-22 | Renaming "ident" into "name" in grammar entries, to prevent confusions. | Hugo Herbelin | |
| We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 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 #13360: Fix incorrect name refreshing when interning a generalized ↵ | coqbot-app[bot] | |
| binder Reviewed-by: herbelin | |||
| 2020-11-17 | Merge PR #13390: Intern application arguments in left-to-right order | coqbot-app[bot] | |
| Reviewed-by: herbelin | |||
| 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 | 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 | 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 #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 | 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-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-10-30 | Renaming Numeral into Number | Pierre Roux | |
| 2020-10-10 | Add location in existential variable names (CEvar/GEvar). | Hugo Herbelin | |
| 2020-09-30 | interp_context_evars: removed unused [shift] argument | Gaëtan Gilbert | |
| Became unused in e034b4090ca45410853db60ae2a5d2f220b48792 | |||
| 2020-08-15 | Document semantic restriction on patterns | Jim Fehrle | |
| 2020-07-17 | Merge PR #12631: Fix record pattern interpretation with implicit arguments | Emilio Jesus Gallego Arias | |
| Reviewed-by: herbelin | |||
| 2020-07-06 | Primitive persistent arrays | Maxime Dénès | |
| Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-07-03 | Fix #11121: Simultaneous definition of term and notation in custom grammar | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |