aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | | | | The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6923: Export optionsGravatar Maxime Dénès2018-03-09
|\ \
| | * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
| * | Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
| | | | | | | | | | | | | | | | | | | | | This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313.
| * | Export the various option localities in the API.Gravatar Pierre-Marie Pédrot2018-03-09
| |/ | | | | | | This prevents relying on an underspecified bool option argument.
* / allow Prop as source for coercionsGravatar charguer2018-03-09
|/
* Merge PR #6941: [toplevel] Respect COQ_COLORS environment variableGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6945: Fix error with univ binders on monomorphic records.Gravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\ \ \ \ \
| | | | * | Fix error with univ binders on monomorphic records.Gravatar Gaëtan Gilbert2018-03-08
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were declared twice for all records. Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an observable error for monomorphic records.
| | | * | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
| | | | * [toplevel] Respect COQ_COLORS environment variableGravatar Thomas Hebb2018-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the toplevel."), the COQ_COLORS environment variable has been ignored, since init_terminal_output unconditionally called init_tag_map with the default colors, overwriting any custom colors that had been previously set. Fix this by creating a separate function, default_styles, to set the default colors. Also, remove the clear_styles function, as it was only called in one place and did nothing (since tag_map is empty to begin with).
* | | | | [vernac] Warn when using “Require” in a sectionGravatar Vincent Laporte2018-03-07
| |_|_|/ |/| | |
* | | | Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \ \ \
* \ \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \
| | | * | | Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | UState normalize -> minimize, Evd nf_constraints -> minimize_universes
| | | * | | Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
| |_|/ / / |/| | | |
* | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | a record.
* \ \ \ \ \ Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
| | | | * | | Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
| | | | | | |
| | | * | | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-03-05
| | | |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
* | | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | * | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
* | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* | | | | | | [toplevel] [vernac] Remove Load hack and check supported scenarios.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Parsing in `VernacLoad` was broken for a while, but the situation has improved by miscellaneous refactoring. However, we still cannot support `Load` properly when proofs are crossing file boundaries. So in this patch we do two things: - We check for supported scenarios [no proofs open at `Load` entry/exit] - Remove the hack in `toplevel` so the behavior of `Load` is consistent between `coqide`/`coqc`. We close #5053 as its main bug was fixed by the main toplevel refactoring and the remaining cases are documented now.
| | * | | | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
| | * | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ / / |/| | |
* | | | Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \ \ \
| * | | | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
| | | | * Adding mention of shelved/given-up status in "Show Existentials".Gravatar Hugo Herbelin2018-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also changed the API of pr_subgoals now using labels. Also removed a trailing space in printing existentials.
* | | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* | | | Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \
* \ \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | | | | | | | | the concl
| | | | * | proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
| |_|_|/ / |/| | | |
| | * | | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | For compatibility, the default is to parse as ident and not as pattern.
| | * | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
| | * | | Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions
| | * | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | Renaming it register_grammars_by_name.
| | * | | More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We generalize the possibility to refer to a notation not only by its "_ U _" form but also using its "a 'U' b". (Wish from EJGA)
| | * | | Being more flexible on format Adding a warning to be more informativeGravatar Hugo Herbelin2018-02-20
| | | | |
| | * | | Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
| | | | |
| | * | | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
| | * | | A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
| | | | |
| | * | | Introducing an intermediary type "constr_prod_entry_key" for grammar ↵Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 21:17:57 +0000