aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-02-13Fixing an anomaly in the presence of "let-in" in the type of a record.Hugo Herbelin
Was raised by Jason on Gitter.
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance ↵Maxime Dénès
information.
2018-02-12Merge PR #6418: More detailed error messages for Canonical Structure, #6398Maxime Dénès
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
This ensures by construction that we never infer constraints outside the variance model.
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
2018-02-06More detailed error messages for Canonical Structure, #6398Paul Steckler
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-30Use r.(p) syntax to print primitive projections.Maxime Dénès
There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-26Support universe instances on the literal TypeTej Chajed
Fixes BZ#5726.
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-03Fix core hint database issue #6521Anton Trunov
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 06:57:43 +0000