aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
| | | | Adding a file fixing #5996 and which uses this feature.
* Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\
* \ Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Maxime Dénès2017-11-03
|\ \
| | * Ltac Debug: exporting env and sigma when needed so that term can be printed.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We do it so as to preserve non-focussing semantics for non-focussing generic arguments. This assumes that the code treats them consistently, which is not enforced statically, but which is reasonable in the sense that when we need a context for printing, we have no other choice as needing a context and we needed one also at interpretation time.
| | * Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786.
| | * Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
| | * Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| | |
| | * Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
| | |
| | * Improving checks about the list separator in tactic notations.Gravatar Hugo Herbelin2017-11-02
| |/ |/| | | | | | | | | | | | | | | | | | | In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep".
| * Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Hugo Herbelin2017-10-30
| | | | | | | | | | | | We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards).
* | Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\ \
* \ \ Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\ \ \ | |_|/ |/| |
| * | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
| | * [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| |/ | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
* / Typo in comment in tactic_matching.ml.Gravatar Hugo Herbelin2017-10-24
|/
* Merge PR #1095: [stm] Remove state handling from FuturesGravatar Maxime Dénès2017-10-20
|\
* | Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | | | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
| * [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
* [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Emilio Jesus Gallego Arias2017-10-15
| | | | The test suite cases are preserved until the feature is actually removed.
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
| | | | | | | | | We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
* Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #1087: [stm] Switch to a functional APIGravatar Maxime Dénès2017-10-09
|\ \
* \ \ Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵Gravatar Maxime Dénès2017-10-09
|\ \ \ | | | | | | | | | | | | Morphism` forms.
* \ \ \ Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\ \ \ \
| | | * | [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
* | | | Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ | | | | | | | | | | | | | | | Compute plugin
| | | * | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence
| | | | * romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
| | | | * Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Gravatar Pierre Letouzey2017-10-05
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega.
* | | / Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Gravatar Pierre Letouzey2017-10-05
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
* | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \
* \ \ \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \ \ \
| | | * | Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-10-04
| |_|/ / |/| | | | | | | | | | | See https://github.com/letouzey/extraction-compute for more details
| | | * Ltac uses the new generic locatable API.Gravatar Pierre-Marie Pédrot2017-10-03
| | | |
| | | * Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
| |_|/ |/| | | | | | | | | | | For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
* | | Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Gravatar Maxime Dénès2017-10-03
|\ \ \
* \ \ \ Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \ \ \
* | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| * | | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
| | | | |
| * | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ / / / | | | | | | | | | | | | | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
| * | | Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
| | | | | | | | | | | | | | | | This commit also fixes range selectors being incorrectly displayed.
| | * | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| |/ / | | | | | | | | | | | | | | | | | | Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
| | * ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| |/
* | Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
* | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
|/ | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
* Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\
* \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ | | | | | | | | | | | | work better on them
| | | * Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|/ |/| |
| | * Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ |/| | | | | | | When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:25:23 +0000