aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-07-04Convert timing tools to run with both python2 and python3Jasper Hugunin
2018-07-03[test suite] Test case for attributesVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Emilio Jesus Gallego Arias
format).
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-28Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Emilio Jesus Gallego Arias
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time.
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Matthieu Sozeau
subtyping.
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-25Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorMaxime Dénès
2018-06-24Adding various tests for mutual records.Pierre-Marie Pédrot
2018-06-23Merge PR #7236: [ssr] simpler semantics for delayed clearsMaxime Dénès
2018-06-22Fix #7704: get_toplevel_path needs normalised argv.(0)Gaëtan Gilbert
When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] test case for rewrite and set on univ poly keysEnrico Tassi
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
It seems that lifting a term with a negative index is not equivalent to strengthening it by applying to a dummy substitution. This looks suspicious at best.
2018-06-20[ssr] test case for rewrite (setoid) making the goal illtypedEnrico Tassi
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
2018-06-17Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵Pierre-Marie Pédrot
to "match").
2018-06-17Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingPierre-Marie Pédrot
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-15Add test-suite case for performance, had to use TimeoutMatthieu Sozeau
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible.
2018-06-15Do not allow spliting in res_pf, this is reserved for pretypingMatthieu Sozeau
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵Pierre-Marie Pédrot
of submodules.
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Matthieu Sozeau
to anomaly)
2018-06-14Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵Matthieu Sozeau
in unification
2018-06-14Merge PR #7771: Tweak printing boxes for unicode bindersHugo Herbelin
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
2018-06-12Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Hugo Herbelin
This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using [].
2018-06-12Fixes #7780 (missing lift in expanding alias under a binder in unification).Hugo Herbelin
2018-06-10Tweak printing boxes for unicode bindersRalf Jung
2018-06-10Fixing #7700 (section variables bound to abbreviations were not found).Hugo Herbelin
Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned.
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
Fix #5012.
2018-06-07add test for #7595Ralf Jung
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
2018-06-05Merge PR #7077: Preserving canonical structure of return predicate in ↵Maxime Dénès
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
2018-06-05Merge PR #7663: test suite: make target to regenerate failing output testsEnrico Tassi
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
2018-06-04Merge PR #7315: An attempt to clarify error message for Arguments needing ↵Maxime Dénès
"rename" flag
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:10:19 +0000