aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-07-07Merge PR #863: Fixing environment in warning "Projection value has no head ↵Maxime Dénès
constant".
2017-07-07Fixing environment in warning "Projection value has no head constant".Hugo Herbelin
Delaying also some computation needed for printing to the time of really printing it.
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Maxime Dénès
with make -j4
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23closing bug #4250Julien Forest
2017-06-23Add tests for handling of warningsTej Chajed
2017-06-22Add test-suite file for funind, extraction with compat 8.6Jason Gross
2017-06-21Should fix a false negative reported by deps-order.sh.Hugo Herbelin
The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
2017-06-20Merge PR#807: romega: fix a slowdownMaxime Dénès
2017-06-19Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalMaxime Dénès
2017-06-19Merge PR#760: Fixing base_include after loc is an option + a better test ↵Maxime Dénès
that #use"include" works
2017-06-19Merge PR#613: Cumulativity for inductive typesMaxime Dénès
2017-06-19Test case for bug 5578.Maxime Dénès
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.
2017-06-16Increase the time limit on 4366.v to make gitlab work better.Gaëtan Gilbert
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Move (part of) tests from checker to successAmin Timany
Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests.
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Change the option to Set Inductive CumulativityAmin Timany
This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
2017-06-16Correct coqchk reductionAmin Timany
2017-06-16Disable debug printingAmin Timany
Fix a mistake in record declaration
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-15Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsMaxime Dénès
2017-06-15Merge PR#752: Adding a test case as requested in bug 5205.Maxime Dénès
2017-06-15Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsMaxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-15Remove dependency on -compat flag in coq_makefile test suite.Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14[typeclasses eauto] Fix bug #3943: non-termination in topologicalMatthieu Sozeau
sorting for the dependency order option.
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-13Merge PR#757: Better sectioning on travis log printing in test-suiteMaxime Dénès
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
2017-06-12Merge PR#709: Bytecode compilation apart from 'make world', againMaxime Dénès
2017-06-12Add support for "-bypass-API" argument of "coq_makefile"Matej Košík
Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
2017-06-12make test-suite/save-logs.sh usable also on old MacOS XMaxime Denes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 15:32:50 +0000