aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-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#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
2017-06-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-06-10Fix Travis sectioningJason Gross
It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right?
2017-06-09Better sectioning on travis log printing in test-suiteJason Gross
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Maxime Dénès
short econstr-cleaning of record.ml
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ↵Maxime Dénès
ssreflect and coq code
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
2017-06-02Merge PR#691: [travis] Add OSX test-suite checking.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 22:14:55 +0000