aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-04-23Merge PR #14161: test-suite: add approve-coqdoc to update all coqdoc output ↵coqbot-app[bot]
files at once Reviewed-by: SkySkimmer
2021-04-23test-suite: add approve-coqdoc to update all coqdoc output files at once.Hugo Herbelin
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-20Merge PR #14131: Check for existence before using `Global.lookup_constant` ↵Pierre-Marie Pédrot
instead of catching `Not_found` Reviewed-by: ppedrot
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-19Check for existence before using `Global.lookup_constant` instead of ↵Lasse Blaauwbroek
catching `Not_found` `Global.lookup_constant` fails with an assertion instead of `Not_found`. Some code relied upon `Not_found`.
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-14Merge PR #14050: Remove remote counter systemcoqbot-app[bot]
Reviewed-by: gares Ack-by: ppedrot Ack-by: ejgallego
2021-04-14Add test for -schedule-vio-checkingGaëtan Gilbert
Close #14074
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
This removes the need for the remote counter.
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
The role of the `zify_saturate` tactic is to augment the goal with positivity constraints. The premisses were previously obtained from the context. If they are not present, we instantiate the saturation lemma anyway. Also, - Remove saturation rules for Z.mul, the reasoning is performed by lia/nia - Run zify_saturate after zify_to_euclidean_division_equations - Better lemma for Z.power - Ensure that lemma are generated once Co-authored-by: Andrej Dudenhefner <mrhaandi> Closes #12184, #11656
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
Reviewed-by: vbgl
2021-04-12[zify] better error reportingBESSON Frederic
The vernacular command takes a reference instead of a constr. Moreover, the head symbol is checked i.e Add Zify InjTyp ref checks that the referenced term has type Intyp X1 ... Xn Closes #14054, #13242 Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
2021-04-08remove `with hintdb` variant of Ltac2 `unify`, becauseSamuel Gruetter
passing one single hintdb is not quite the right API, we should pass a transparent state instead, but that would require an API for manipulating hintdbs and transparent states, postponing
2021-04-07unify for Ltac2Samuel Gruetter
Fixes #14083
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04Fixing #13581: missing support for let-ins in arity of inductive types.Hugo Herbelin
At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure.
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-31Merge PR #14035: Fix printing of ssr do intros and seq tacticscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: ppedrot
2021-03-31Fix printing of ssr do intros and seq tacticsLasse Blaauwbroek
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections.
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-26Add non-performance-based testJason Gross
2021-03-26Be more thorough when testing PArray.set.Guillaume Melquiond
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
Bytecode execution of persistent arrays can modify structured values meant to be marshalled in vo files. Some VM values are not marshallable, leading to this anomaly. There are further issues with the use of a hash table to store structured values, since they rely on structural equality and hashing functions. Persistent arrays are not safe in this context. Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]
Reviewed-by: gares
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths ↵coqbot-app[bot]
to check for conversion Reviewed-by: gares Ack-by: SkySkimmer
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-25Fix the redeclaration check for Ltac2 entry points.Pierre-Marie Pédrot
Fixes #14003: Ltac2 redefinition check is broken.
2021-03-24Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-22Merge PR #13961: Implement ! goal selector for Ltac2.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-19implement is_const, is_var, ... etc and has_evar for Ltac2Samuel Gruetter
Fixes #13963
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are ↵Pierre-Marie Pédrot
transitively closed Reviewed-by: ppedrot
2021-03-18Implement ! goal selector for Ltac2.Pierre-Marie Pédrot
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
2021-03-16Slightly richer API allowing to shift the inductive in a block.Pierre-Marie Pédrot
2021-03-16Add tests for the new Ltac2 Ind API.Pierre-Marie Pédrot
2021-03-13Allow scope delimiters in Ltac2 open_constr:(...) quotation.Pierre-Marie Pédrot
Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.
2021-03-13Minimize the set of multiple inheritance paths to check for conversionKazuhiko Sakaguchi
The table of coercion classes (`class_tab`) has been extended with information about reachability. The conversion checking of a pair of multiple inheritance paths (of coercions) will be skipped if these paths can be reduced to smaller adjoining pairs of multiple inheritance paths, and this reduction will be determined based on that reachability information.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:24 +0000