aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01Implementing support for vos/vok files.charguer
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
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-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-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
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive ↵Frédéric Besson
projections Reviewed-by: fajb
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:39:54 +0000