aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-01-31Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Maxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-25Add test case for #5747Maxime Dénès
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Maxime Dénès
for primitive projections
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
2018-01-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-13Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSMaxime Dénès
2018-01-12Merge PR #6483: Strong invariants in polymorphic definitionsMaxime Dénès
2018-01-11Document test-suite PRINT_LOGS.Gaëtan Gilbert
2018-01-11Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGaëtan Gilbert
PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1
2018-01-11Merge PR #6557: First stab at documenting the test suite.Maxime Dénès
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else.
2018-01-11Lint and remove redundant lineJasper Hugunin
2018-01-10Add comments by @psteckler to test-suite/README.mdJasper Hugunin
2018-01-08Merge PR #6497: Add optimize_heap tactic for #6488Maxime Dénès
2018-01-08Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsMaxime Dénès
2018-01-07Mention -B argument of make to rerun testsJasper Hugunin
2018-01-06First stab at documenting the test suite.Jasper Hugunin
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
2017-12-31Trim more trailing whitespace in coq-makefile timing testJason Gross
Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces
2017-12-27Add TIMING_SORT_BY and --sort-by to timing scriptsJason Gross
This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
2017-12-20Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).Maxime Dénès
2017-12-20Merge PR #6234: Make the micromega extraction check a regular output test.Maxime Dénès
2017-12-19Fix ltacprof_abstract (I think because of #6411 parallel merge).Gaëtan Gilbert
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Maxime Dénès
Extraction Language command
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-15Do dependencies in 1 command per file class.Gaëtan Gilbert
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
Universe instances were lost during constructions of the canonical instance.
2017-12-14Make [abstract] nodes show up in the Ltac profileJason Gross
This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise.
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6379: Fix profiling pluginMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 16:04:17 +0000