aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-21Add a generated file to .gitignoreJason Gross
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-20Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's LtacAnton Trunov
Reviewed-by: anton-trunov
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-19Merge PR #12502: Preserve sharing in evar instancesGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2020-06-19Add overlays.Pierre-Marie Pédrot
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
It is only used for this kind of hints, never for Extern / Unfold.
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-06-19Remove access to hint section variables.Pierre-Marie Pédrot
The only use was seemingly a bug introduced in 0aec9033a by an accidental variable capture. There is indeed no reason that the set of variables of a hint corresponds to the one of the current environment.
2020-06-19Opacify the type of hint metadata.Pierre-Marie Pédrot
2020-06-19Remove dead code in the Hints API.Pierre-Marie Pédrot
2020-06-19Do not export Hints.make_extern.Pierre-Marie Pédrot
2020-06-19Do not export flags in Hints.make_resolves.Pierre-Marie Pédrot
They are always the same.
2020-06-19Do not be verbose when declaring subclass hints.Pierre-Marie Pédrot
There is no point in warning about eauto being the only one able to use those hints, since they will be used by typeclass_eauto instead. It was probably an oversight introduced quite a long time ago.
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
They were always instantiated with the triple (true, false, false).
2020-06-19Try to preserve more sharing in nf_evars_and_universes_opt_subst.Pierre-Marie Pédrot
2020-06-19Share the identity instance in pretyping environments.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
Instead of costly linear reallocations, we share as much as possible of the prefixes of the various environment subcomponents.
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-18Merge PR #12536: tactics.rst: fix typo — readd `cbv` to title of its sectionThéo Zimmermann
Reviewed-by: jfehrle
2020-06-17[ci] Use a tested branch of PerennialTej Chajed
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-06-17Merge PR #12506: [toplevel] Annotate tailcall functionsEnrico Tassi
Reviewed-by: maximedenes
2020-06-17Use an efficient data structure for VM compilation indexing.Pierre-Marie Pédrot
2020-06-17Check duplicity of constructor names in an algorithmically efficient way.Pierre-Marie Pédrot
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
Fixes #12529
2020-06-16Use evar clauses instead of meta clauses in Autorewrite hint registration.Pierre-Marie Pédrot
This is barely more meaningful but at least we do not rely on an antiquated API now.
2020-06-16Code simplification in Autorewrite.Pierre-Marie Pédrot
2020-06-16Remove dead code in autorewrite.Pierre-Marie Pédrot
2020-06-16make the linter happyEnrico Tassi
2020-06-15Merge PR #12509: updated ci for unicoqThéo Zimmermann
Reviewed-by: Zimmi48
2020-06-15updated ci for unicoqbeta
2020-06-15Merge PR #11906: [micromega] native support for boolean operatorsMaxime Dénès
Reviewed-by: maximedenes Reviewed-by: pi8027 Reviewed-by: vbgl
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-15[ssr] remove catch allEnrico Tassi
2020-06-15Merge PR #12494: [dev/ci/nix] Support for building the Gappa plugin.Vincent Laporte
Reviewed-by: vbgl
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-14Update theories/micromega/ZifyBool.vFrédéric Besson
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
This will ensure that we don't introduce problems as it has happened in the past. While we are at it, we fix one easy case of non-tail call.
2020-06-12Merge PR #12357: [declare] Remove some unused `fix_exn`Enrico Tassi
Reviewed-by: gares
2020-06-12Merge PR #12498: [dune] [dbg] Fix coqide target after CoqIDE move.Maxime Dénès
Reviewed-by: maximedenes
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
2020-06-11[stm] Simplify logic involving forced futures.Emilio Jesus Gallego Arias
After the previous commit, we don't need to chain a dummy future anymore.
2020-06-11[declare] Remove some unused `fix_exn`Emilio Jesus Gallego Arias
In the current proof save path, the kernel can raise an exception when checking a proof wrapped into a future. However, in this case, the future itself will "fix" the produced exception, with the mandatory handler set at the future's creation time. Thus, there is no need for the declare layer to mess with exceptions anymore, if my logic is correct. Note that the `fix_exn` parameter to the `Declare` API was not used anymore. This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from pre-github times, so unfortunately I didn't have access to the discussion. We need to be careful in `perform_buildp` as to catch the `Qed` error and properly notify the STM about it with `State.exn_on`; this was previously done by the declare layer using a hack [grabbing internal state of the future, that the future itself was not using as it was already forced], but we now do it in the caller in a more principled way. This has been tested in the case that tactics succeed but Qed fails asynchronously.
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-06-11Merge PR #12492: Fix Windows addons.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-11[dune] [dbg] Fix coqide target after CoqIDE move.Emilio Jesus Gallego Arias
Fixes #12496
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 12:19:31 +0000