aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-23Use the unification result for eauto's eapply.Pierre-Marie Pédrot
Instead of dropping the unification result and calling simple eapply with the original term, we simply use the same code path as auto and typeclass eauto, i.e. reuse the clenv for refinement.
2020-06-22Merge PR #12520: Cleanup the autorewrite implementationHugo Herbelin
Reviewed-by: herbelin
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential ↵Gaëtan Gilbert
variables in goals Reviewed-by: SkySkimmer
2020-06-22Merge PR #12555: Add test-suite/redirect_test.out file to .gitignoreGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-22Merge PR #12546: [ci] Use a tested branch of PerennialEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-21Merge PR #12505: Cleanup the Hints APIHugo Herbelin
Reviewed-by: herbelin
2020-06-21Merge PR #12559: Add index for coqdoc.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-06-21Add index for coqdoc.Théo Zimmermann
Fixes #12545.
2020-06-21Add a generated file to .gitignoreJason Gross
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:01:53 +0000