aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-08-17Merge PR #12802: Document semantic restriction on patterns in Gallina match ↵coqbot
construct Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.)
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non ↵Pierre-Marie Pédrot
purely applicative stacks Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-08-13Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred.Enrico Tassi
Reviewed-by: gares
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
Reviewed-by: anton-trunov
2020-08-13Merge PR #12720: Factor code related to class hint clenvHugo Herbelin
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2020-08-13Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets.Hugo Herbelin
Reviewed-by: herbelin
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
Reviewed-by: erikmd Reviewed-by: herbelin
2020-08-13Merge PR #12479: Bring Int63 notations into line with stdlibAnton Trunov
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-12Merge PR #12748: Windows CI: changed cygwin repo servercoqbot
Reviewed-by: Zimmi48
2020-08-12Add overlays.Pierre-Marie Pédrot
2020-08-12Cosmetic changes as suggested by SkySkimmer.Pierre-Marie Pédrot
2020-08-12Further code simplification in typeclass resolution tactic.Pierre-Marie Pédrot
2020-08-12Split the uses of connect_hint_clenv into two different functions.Pierre-Marie Pédrot
The first one is encapsulating the clenv part, and is now purely internal, while the other one provides an abstract interfact to get fresh term instances from a hint.
2020-08-12Remove dead code after the previous commit.Pierre-Marie Pédrot
The costly universe refreshing functions were only used for typeclass hint resolution, which now relies on the provided hint context.
2020-08-12Tentatively more efficient implementation of e_give_exact for typeclasses.Pierre-Marie Pédrot
The old code was refreshing the whole evarmap when only the constraints introduced by the term would matter. Since exact hints never introduces metas for missing binders, there is nothing to extract from the clenv, so we can just generate a fresh universe substitution.
2020-08-12Export a dedicated function that applies immediately a hint.Pierre-Marie Pédrot
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
We inline the clenv universe refreshing, since it was the only place in the code that used it. Furthermore it was performing useless substitutions in the clenv.
2020-08-12Make the Hint.hint type private.Pierre-Marie Pédrot
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-08-12Do not do a round trip with auto hint representation in autoapply.Pierre-Marie Pédrot
2020-08-12Do not tamper with hints in Class_tactics.with_prods.Pierre-Marie Pédrot
2020-08-12Perfom an goal enter in the relevant class tactics instead of outside.Pierre-Marie Pédrot
2020-08-12Inline Class_tactics.clenv_of_prods.Pierre-Marie Pédrot
It was unnecessarily obfuscated.
2020-08-12Additional statements about List.repeatOlivier Laurent
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
2020-08-12Windows CI: changed cygwin repo serverMichael Soegtrop
2020-08-11add deprecation to changelogYishuai Li
2020-08-11deprecate prod_curry and prod_uncurryYishuai Li
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot
2020-08-11Small code simplification in contract_(co)fix.Pierre-Marie Pédrot
Probably a remnant of a time where the difference in code path was relevant.
2020-08-11Move reduce_mind_case from Reductionops to Tacred.Pierre-Marie Pédrot
It was only used there, and its API required to export an ad-hoc type to represent pattern-matchings.
2020-08-11Merge PR #12794: Repair coqide option "Display parentheses"Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
Reviewed-by: vbgl
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
Reviewed-by: vbgl
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[micromega] Fix bug#12790Frédéric Besson
zify used to generate many syntactic positivity constraints when translating a goal from nat to Z. For instance, to state that the product of 2 integers is positive. Instead, lia performs an interval analysis that is more semantic. The bug was that the interval analysis was performed after the elimination of equations. The current workaround is to perform interval analysis before and after eliminating equations. bla
2020-08-10[zify] fix for bug#12791Frédéric Besson
The elimination of let bindings is performing a convertibility check in order to deal with type aliases.
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Int63 notations into line with stdlibJason Gross
We also put them in a module, so users can `Require Int63. Import Int63.Int63Notations` without needing to unqualify the primitives. In particular, we change - `a \% m` into `a mod m` to correspond with the notation in ZArith - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere - `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation The old notations are still accessible as deprecated notations. Fixes #12454
2020-08-09Bring Float notations in line with stdlibJason Gross
This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
2020-08-08Merge PR #12796: [default.nix] Propagate dependency on num following #12604.Vincent Laporte
Reviewed-by: vbgl
2020-08-07[default.nix] Propagate dependency on num following #12604.Théo Zimmermann
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61.
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵coqbot
environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-06Merge PR #12782: Trying to rephrase complex sentences to make them easier to ↵coqbot
read. Reviewed-by: jfehrle Ack-by: Mbodin Ack-by: corwin-of-amber
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-06Repair coqide option "Display parentheses"Jean-Christophe Léchenet
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 02:36:16 +0000