aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison.
2019-11-01Add tests for primitive floats with 'vm_compute'Guillaume Bertholon
Tests are updated to include VM computations and check for double rounding.
2019-11-01Add tests for primitive floatsGuillaume Bertholon
Add utility ldexp and frexp functions to prevent dealing with the shift of ldshiftexp and frshiftexp everywhere. Also move primitive integer tests to place all primitive tests in the same directory.
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
(namely, [RewriteRelation]s beyond Equivalence ones) Thanks to @CohenCyril for suggesting this enhancement
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
* Preserve the same behavior/interface but merge the two Module Types (UNDER_EQ and) UNDER_REL. * Remove the "Reflexive" argument in Under_rel.Under_rel * Update plugin code (ssrfwd.ml) & Factor-out the main step * Update the Hint (viz. apply over_rel_done => apply: over_rel_done) * All the tests still pass! Credits to @CohenCyril for suggesting this enhancement
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
Ack-by: SkySkimmer Ack-by: proux01 Reviewed-by: vbgl
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: jfehrle
2019-10-31Fix #8459: anomaly not enough abstractions in fix bodyGaëtan Gilbert
We reach the anomaly because we call check_fix on a surrounding fixpoint from the pretyper, and the inner fix hasn't been checked. Using whd_all isn't useful in the specific reported case but a case where it's necessary can probably be crafted. See also #11013
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
Noticed by coverage, test code by Gäetan Gilbert. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
Ack-by: JasonGross Reviewed-by: ejgallego
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
Close #4502
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin
2019-10-29Show diffs in "Show Proof."Jim Fehrle
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them.
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-28Fix #10903: type-in-type allows fixpoints on sprop inductivesGaëtan Gilbert
I still don't know why it produces a Not_found instead of a regular error in coqtop but let's forget about it.
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵Pierre-Marie Pédrot
the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for ↵Enrico Tassi
dune-compiled Coq Reviewed-by: gares
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
More precisely: The equivalent in #7288 (4dab4fc) to the former call to ltac_interp_name_env was not done anymore when interpreting uconstr's.
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
This lets the checker verify that we didn't produce nonsense.
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
Reviewed-by: herbelin
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
This is the dual of #10344.
2019-10-17Fix Locate printing regressionGuillaume Melquiond
Fixes #9428. (Again.) This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them. Corrects a 8.9.1 → 8.10.0 regression. (cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
Opening up a lambda should always lift the substitution attached to it.
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
AFAICT there is no reason to use interp_open_constr I used Evd.from_ctx to keep passing evar maps around but maybe we should be passing ustates instead?
2019-10-14test-suite/Makefile: work when manually involved for dune-compiled CoqGaëtan Gilbert
i.e. you can do ~~~ make -f Makefile.dune world make -C test-suite success ~~~ to make just the success tests, then modify Coq sources and retest just the ones you want
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: hendriktews Reviewed-by: herbelin Ack-by: mattam82
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint ↵Pierre-Marie Pédrot
database Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ↵Pierre-Marie Pédrot
sections Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 06:09:15 +0000