aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on ↵Gaëtan Gilbert
applications Reviewed-by: SkySkimmer
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
This fixes an incompleteness of subtyping on cumulative inductives, where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation depending on the variance of I's universe.
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
(NB: this needs relevance mark fixing)
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
Reviewed-by: gares
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵Emilio Jesus Gallego Arias
record Reviewed-by: ejgallego
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
This causes the makefile to break due to dependencies when it fails, and it's not worth adding a whole mess of code to catch the failure for these files.
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-03-01Set COQLIB so the test suite will run locally on Windows.Jim Fehrle
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
This is intended to be separate from handling of implicit binders. The remaining uses of declare_manual_implicits satisfy a lot of assertions, giving the possibility of simplifying the interface in the future. Two disabled warnings are added for things that currently pass silently. Currently only Mtac passes non-maximal implicits to declare_manual_implicits with the force-usage flag set. When implicit arguments don't have to be named, should move Mtac over to set_implicits.
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25add testcase for primitive projectionEnrico Tassi
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-25add testcase for fixEnrico Tassi
2019-02-25add test case for "match"Enrico Tassi
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars.
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: herbelin Reviewed-by: mattam82
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
Parameters had to be removed in cases_pattern_of_glob_constr.
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
This is because it can raise Not_found in depth and we need to catch it at the right time.
2019-02-19Fix #9595: missing non-primitive-record warning with 0 field recordGaëtan Gilbert
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-02-18Merge PR #9439: Separate variance and universe fields in inductives.Pierre-Marie Pédrot
Ack-by: ppedrot
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ↵Maxime Dénès
and primititive projections Reviewed-by: maximedenes
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
I think the usage looks cleaner this way.
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-02-13Merge PR #9554: Don't save expected failure logs from opened/ bugs.Maxime Dénès
Reviewed-by: maximedenes
2019-02-13more testsEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
(when defining a new constant)
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
Reviewed-by: CohenCyril Fixes a bug introduced by PR #9341
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:55:24 +0000