Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | 2018-01-31 | |
|\ | |||
* \ | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | 2018-01-31 | |
|\ \ | |||
* | | | Add test case for #5286. | 2018-01-29 | |
| | | | |||
| | * | Add test case for #5747 | 2018-01-25 | |
| |/ |/| | |||
* | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵ | 2018-01-23 | |
|\ \ | | | | | | | | | | for primitive projections | ||
* \ \ | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | 2018-01-22 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | 2018-01-22 | |
|\ \ \ \ | |||
| | | * | | Adding a test for coqchk bug #6619. | 2018-01-20 | |
| |_|/ / |/| | | | |||
| * | | | Add test-suite file for issue #6617. | 2018-01-19 | |
| | | | | |||
* | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | 2018-01-18 | |
|\ \ \ \ | |/ / / |/| | | | |||
* | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | 2018-01-17 | |
|\ \ \ \ | |||
| | | * | | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | 2018-01-17 | |
| | | | | | |||
| | * | | | Add a test that `prod_applist_assum` reduces the right number of let-ins | 2018-01-17 | |
| | | | | | |||
| | * | | | Use let-in aware prod_applist_assum in dtauto and firstorder. | 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 | 2018-01-16 | |
|\ \ \ \ | |_|/ / |/| | | | |||
| * | | | More tests on brackets with goal selectors (including failures). | 2018-01-15 | |
| | | | | |||
| * | | | Add test-suite file for bracket with goal selector. | 2018-01-15 | |
| | | | | |||
* | | | | Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 2018-01-13 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6483: Strong invariants in polymorphic definitions | 2018-01-12 | |
|\ \ \ \ \ | |||
| | * | | | | Document test-suite PRINT_LOGS. | 2018-01-11 | |
| | | | | | | |||
| | * | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGS | 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. | 2018-01-11 | |
|\ \ \ \ \ | |||
| | * | | | | Force polymorphic definitions to have no internal constraints. | 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 | 2018-01-11 | |
| | | | | | |||
| * | | | | Add comments by @psteckler to test-suite/README.md | 2018-01-10 | |
| | | | | | |||
* | | | | | Merge PR #6497: Add optimize_heap tactic for #6488 | 2018-01-08 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | 2018-01-08 | |
|\ \ \ \ \ \ | |||
| | | * | | | | Mention -B argument of make to rerun tests | 2018-01-07 | |
| | | | | | | | |||
| | | * | | | | First stab at documenting the test suite. | 2018-01-06 | |
| | | |/ / / | |||
| | * | | | | add optimize_heap tactic for #6488 | 2018-01-03 | |
| | | | | | | |||
| | | | | * | Cleanup name-binding structure for fresh evar name generation. | 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 | 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 | 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 | 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). | 2017-12-20 | |
|\ \ | |||
* \ \ | Merge PR #6234: Make the micromega extraction check a regular output test. | 2017-12-20 | |
|\ \ \ | |||
| | * | | Fix ltacprof_abstract (I think because of #6411 parallel merge). | 2017-12-19 | |
| |/ / |/| | | |||
* | | | Merge PR #6400: Circle CI | 2017-12-19 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6436: Fix #5368: Canonical structure unification fails. | 2017-12-18 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6406: Make [abstract] nodes show up in the Ltac profile | 2017-12-18 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | 2017-12-18 | |
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | Extraction Language command | ||
* \ \ \ \ \ \ \ | Merge PR #6217: Do dependencies in 1 command per file class. | 2017-12-18 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | 2017-12-18 | |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | Do dependencies in 1 command per file class. | 2017-12-15 | |
| | | | | | | | | | | |||
| | | | | | * | | | | Fix #5368: Canonical structure unification fails. | 2017-12-15 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Universe instances were lost during constructions of the canonical instance. | ||
| | | | | * | | | | Make [abstract] nodes show up in the Ltac profile | 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 | 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 | 2017-12-14 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6379: Fix profiling plugin | 2017-12-14 | |
|\ \ \ \ \ \ \ \ |