aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Collapse)AuthorAge
* Merge PR #7152: [api] Remove dependency of library on Vernacexpr.Gravatar Pierre-Marie Pédrot2018-04-23
|\
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Gravatar Pierre-Marie Pédrot2018-04-13
|\ \ | | | | | | | | | contains evars
* | | Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Hugo Herbelin2018-04-12
| | | | | | | | | | | | | | | The "Stream.Error" printer does add a period, so, the messages themselves should not.
| | * [api] Remove dependency of library on Vernacexpr.Gravatar Emilio Jesus Gallego Arias2018-04-06
| |/ |/| | | | | | | | | | | | | | | Morally, `library` should not depend on the vernacular definition. This will also create problems when trying to modularize the codebase due to the cycle [vernacs depend for example on constrexprs]. The fix is fortunately easy.
* | Merge PR #7016: Make parsing independent of the cumulativity flag.Gravatar Enrico Tassi2018-04-05
|\ \
* \ \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \ \
| * | | [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
| | | | | | | | | | | | | | | | | | | | | | | | This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack.
| | | * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
* / | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/ /
* | Merge PR #7062: Slightly refining some error messages about unresolvable evars.Gravatar Pierre-Marie Pédrot2018-03-27
|\ \
| * | Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| | | | | | | | | | | | For instance, error in "Goal forall a f, f a = 0" is now located.
| | * bool option -> (VernacCumulative | VernacNonCumulative) optionGravatar Gaëtan Gilbert2018-03-22
| | |
| | * Make parsing independent of the cumulativity flag.Gravatar Gaëtan Gilbert2018-03-21
| |/
* / [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/ | | | | | This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
* [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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 12:03:44 +0000