Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | Maxime Dénès | 2018-01-31 |
|\ | |||
* \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | 2018-01-31 |
|\ \ | |||
* | | | Add test case for #5286. | Maxime Dénès | 2018-01-29 |
| | | | |||
| | * | Add test case for #5747 | Maxime Dénès | 2018-01-25 |
| |/ |/| | |||
* | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵ | Maxime Dénès | 2018-01-23 |
|\ \ | | | | | | | | | | for primitive projections | ||
* \ \ | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | 2018-01-22 |
|\ \ \ | |||
* \ \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | Maxime Dénès | 2018-01-22 |
|\ \ \ \ | |||
| | | * | | Adding a test for coqchk bug #6619. | Pierre-Marie Pédrot | 2018-01-20 |
| |_|/ / |/| | | | |||
| * | | | Add test-suite file for issue #6617. | Cyprien Mangin | 2018-01-19 |
| | | | | |||
* | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | Maxime Dénès | 2018-01-18 |
|\ \ \ \ | |/ / / |/| | | | |||
* | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | Maxime Dénès | 2018-01-17 |
|\ \ \ \ | |||
| | | * | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | Jasper Hugunin | 2018-01-17 |
| | | | | | |||
| | * | | | Add a test that `prod_applist_assum` reduces the right number of let-ins | Jasper Hugunin | 2018-01-17 |
| | | | | | |||
| | * | | | Use let-in aware prod_applist_assum in dtauto and firstorder. | Jasper Hugunin | 2018-01-17 |
| | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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). | ||
* | | | | Merge PR #6551: Bracket with goal selector | Maxime Dénès | 2018-01-16 |
|\ \ \ \ | |_|/ / |/| | | | |||
| * | | | More tests on brackets with goal selectors (including failures). | Théo Zimmermann | 2018-01-15 |
| | | | | |||
| * | | | Add test-suite file for bracket with goal selector. | Théo Zimmermann | 2018-01-15 |
| | | | | |||
* | | | | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | Maxime Dénès | 2018-01-13 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6483: Strong invariants in polymorphic definitions | Maxime Dénès | 2018-01-12 |
|\ \ \ \ \ | |||
| | * | | | | Document test-suite PRINT_LOGS. | Gaëtan Gilbert | 2018-01-11 |
| | | | | | | |||
| | * | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | Gaëtan Gilbert | 2018-01-11 |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1 | ||
* | | | | | Merge PR #6557: First stab at documenting the test suite. | Maxime Dénès | 2018-01-11 |
|\ \ \ \ \ | |||
| | * | | | | Force polymorphic definitions to have no internal constraints. | Pierre-Marie Pédrot | 2018-01-11 |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| * | | | | Lint and remove redundant line | Jasper Hugunin | 2018-01-11 |
| | | | | | |||
| * | | | | Add comments by @psteckler to test-suite/README.md | Jasper Hugunin | 2018-01-10 |
| | | | | | |||
* | | | | | Merge PR #6497: Add optimize_heap tactic for #6488 | Maxime Dénès | 2018-01-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | Maxime Dénès | 2018-01-08 |
|\ \ \ \ \ \ | |||
| | | * | | | | Mention -B argument of make to rerun tests | Jasper Hugunin | 2018-01-07 |
| | | | | | | | |||
| | | * | | | | First stab at documenting the test suite. | Jasper Hugunin | 2018-01-06 |
| | | |/ / / | |||
| | * | | | | add optimize_heap tactic for #6488 | Paul Steckler | 2018-01-03 |
| | | | | | | |||
| | | | | * | Cleanup name-binding structure for fresh evar name generation. | Pierre-Marie Pédrot | 2018-01-02 |
| | | | |/ | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | / | | Trim more trailing whitespace in coq-makefile timing test | Jason Gross | 2017-12-31 |
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces | ||
| * | | | Add TIMING_SORT_BY and --sort-by to timing scripts | Jason Gross | 2017-12-27 |
| |/ / | | | | | | | | | | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 | ||
* / / | [API] remove large file containing duplicate interfaces | Enrico Tassi | 2017-12-27 |
|/ / | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | ||
* | | Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge). | Maxime Dénès | 2017-12-20 |
|\ \ | |||
* \ \ | Merge PR #6234: Make the micromega extraction check a regular output test. | Maxime Dénès | 2017-12-20 |
|\ \ \ | |||
| | * | | Fix ltacprof_abstract (I think because of #6411 parallel merge). | Gaëtan Gilbert | 2017-12-19 |
| |/ / |/| | | |||
* | | | Merge PR #6400: Circle CI | Maxime Dénès | 2017-12-19 |
|\ \ \ | |||
* \ \ \ | Merge PR #6436: Fix #5368: Canonical structure unification fails. | Maxime Dénès | 2017-12-18 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6406: Make [abstract] nodes show up in the Ltac profile | Maxime Dénès | 2017-12-18 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès | 2017-12-18 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | Maxime Dénès | 2017-12-18 |
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | Extraction Language command | ||
* \ \ \ \ \ \ \ | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | 2017-12-18 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | Maxime Dénès | 2017-12-18 |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | Do dependencies in 1 command per file class. | Gaëtan Gilbert | 2017-12-15 |
| | | | | | | | | | | |||
| | | | | | * | | | | Fix #5368: Canonical structure unification fails. | Pierre-Marie Pédrot | 2017-12-15 |
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Universe instances were lost during constructions of the canonical instance. | ||
| | | | | * | | | | Make [abstract] nodes show up in the Ltac profile | Jason Gross | 2017-12-14 |
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| | | | * | | | | Add tactics to reset and display the Ltac profile | Jason Gross | 2017-12-14 |
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is useful for tactics that run a bunch of tests and need to display the profile for each of them. | ||
* | | | | | | | Merge PR #6386: Catch errors while coercing 'and' intro patterns | Maxime Dénès | 2017-12-14 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6379: Fix profiling plugin | Maxime Dénès | 2017-12-14 |
|\ \ \ \ \ \ \ \ |