aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Gravatar Maxime Dénès2018-01-31
|\
* \ Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \
* | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | * Add test case for #5747Gravatar Maxime Dénès2018-01-25
| |/ |/|
* | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Gravatar Maxime Dénès2018-01-23
|\ \
* \ \ Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \ \
* \ \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \ \
| | | * | Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
| |_|/ / |/| | |
| * | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
* | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ | |/ / / |/| | |
* | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \
| | | * | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| | * | | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | * | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| | |/ /
* | | | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \ \ | |_|/ / |/| | |
| * | | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| * | | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
* | | | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Maxime Dénès2018-01-13
|\ \ \ \
* \ \ \ \ Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \ \
| | * | | | Document test-suite PRINT_LOGS.Gravatar Gaëtan Gilbert2018-01-11
| | * | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Gaëtan Gilbert2018-01-11
| |/ / / / |/| | | |
* | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \
| | * | | | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| |/ / / / |/| | | |
| * | | | Lint and remove redundant lineGravatar Jasper Hugunin2018-01-11
| * | | | Add comments by @psteckler to test-suite/README.mdGravatar Jasper Hugunin2018-01-10
* | | | | Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \
| | | * | | | Mention -B argument of make to rerun testsGravatar Jasper Hugunin2018-01-07
| | | * | | | First stab at documenting the test suite.Gravatar Jasper Hugunin2018-01-06
| | | |/ / /
| | * | | | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
| | | | | * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| | | | |/ | | | |/|
* | | / | Trim more trailing whitespace in coq-makefile timing testGravatar Jason Gross2017-12-31
| |_|/ / |/| | |
| * | | Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Jason Gross2017-12-27
| |/ /
* / / [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
|/ /
* | Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).Gravatar Maxime Dénès2017-12-20
|\ \
* \ \ Merge PR #6234: Make the micromega extraction check a regular output test.Gravatar Maxime Dénès2017-12-20
|\ \ \
| | * | Fix ltacprof_abstract (I think because of #6411 parallel merge).Gravatar Gaëtan Gilbert2017-12-19
| |/ / |/| |
* | | Merge PR #6400: Circle CIGravatar Maxime Dénès2017-12-19
|\ \ \
* \ \ \ Merge PR #6436: Fix #5368: Canonical structure unification fails.Gravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6406: Make [abstract] nodes show up in the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6217: Do dependencies in 1 command per file class.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingGravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \ \ \ \
| | * | | | | | | | Do dependencies in 1 command per file class.Gravatar Gaëtan Gilbert2017-12-15
| | | | | | * | | | Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
| |_|_|_|_|/ / / / |/| | | | | | | |
| | | | | * | | | Make [abstract] nodes show up in the Ltac profileGravatar Jason Gross2017-12-14
| |_|_|_|/ / / / |/| | | | | | |
| | | | * | | | Add tactics to reset and display the Ltac profileGravatar Jason Gross2017-12-14
| |_|_|/ / / / |/| | | | | |
* | | | | | | Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6379: Fix profiling pluginGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 02:59:22 +0000