aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-09Fixing a coercion entry transitivity bug.Hugo Herbelin
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-06Add a few comments about the code.Pierre-Marie Pédrot
2020-08-06Actually update uninitialized evar instances (hum hum).Pierre-Marie Pédrot
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Store the default instance in named_context_val.Pierre-Marie Pédrot
This is not pretty but I do not see how to do this in a way that is both backwards compatible and efficient.
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-08-06Fast path for evar substitution relying on evar identity substitutions.Pierre-Marie Pédrot
2020-08-06Remove several calls to Evarutil.new_pure_evar.Pierre-Marie Pédrot
2020-08-06Store the default evar instance inside the evar info.Pierre-Marie Pédrot
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
2020-08-05Merge PR #12724: CI metacoq: make .merlincoqbot
Reviewed-by: Zimmi48
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-04Merge PR #12706: Mention coqbot minimize feature in issue template.coqbot
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: jtcoolen
2020-08-04Mention coqbot minimize feature in issue template.Julien Coolen
This allows coqbot to reply back with a minimized version of some code reproducing a bug, using the coq-bug-minimizer program from Jason Gross. See https://github.com/JasonGross/coq-tools#coq-bug-minimizer.
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-08-03Merge PR #12772: coqdoc: Fix the “details” environmentLi-yao Xia
Reviewed-by: Lysxia
2020-07-30Merging is now possible with coqbot.Théo Zimmermann
This is proposed as an alternative to the merge script, in particular for maintainers without a GPG key.
2020-07-30Merge PR #12767: Fix do in ssreflect-proof-language.rstcoqbot
Reviewed-by: Zimmi48
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again.
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-28Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc indexLi-yao Xia
Reviewed-by: Lysxia
2020-07-27Do not rely on higher-order interfaces for patterns in dnets.Pierre-Marie Pédrot
The old API was taking a function to decompose constr patterns into dnet patterns, but it was applying it in an eager way. So there is not point in exposing such a complex interface. Instead, we make explicit the dnet pattern type, export a function that turns a constr pattern into a dnet pattern, and make the add and remove dnet functions take a dnet pattern instead. This only affects pattern-consuming functions. The lookup function, which operates on kernel terms instead of constr patterns, is still relying on HO primitives.
2020-07-27Merge PR #12729: Faster algorithm to compute algebraic universe mapping in ↵Gaëtan Gilbert
minimization. Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 20:57:15 +0000