aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | The function turning a side-effect declaration into the corresponding entry was crazily wrong, as it used a named universe context quantifying over DeBruijn universe indices. Declaring such entries resulted in random anomalies. This fixes bug #5641.
* Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
* Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
* | Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \
| * | closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
| | |
* | | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Gravatar Maxime Dénès2017-06-27
|\ \ \ | | | | | | | | | | | | with make -j4
* \ \ \ Merge PR#826: Put plugin exports in the right compatibility fileGravatar Maxime Dénès2017-06-26
|\ \ \ \
* \ \ \ \ Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\ \ \ \ \ | | |_|/ / | |/| | |
* | | | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \ \ \
| | * | | | closing bug #4250Gravatar Julien Forest2017-06-23
| |/ / / / |/| | | |
| | | | * Add tests for handling of warningsGravatar Tej Chajed2017-06-23
| | | | |
| | * | | Add test-suite file for funind, extraction with compat 8.6Gravatar Jason Gross2017-06-22
| |/ / / |/| | |
| | * | Should fix a false negative reported by deps-order.sh.Gravatar Hugo Herbelin2017-06-21
| |/ / |/| | | | | | | | | | | | | | | | | The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
* | | Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\ \ \
* \ \ \ Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\ \ \ \
* \ \ \ \ Merge PR#760: Fixing base_include after loc is an option + a better test ↵Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | that #use"include" works
* \ \ \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \
* | | | | | | Test case for bug 5578.Gravatar Maxime Dénès2017-06-19
| | | | | | |
| | | | * | | romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | Increase the time limit on 4366.v to make gitlab work better.Gravatar Gaëtan Gilbert2017-06-16
| |_|_|/ / / |/| | | | |
| * | | | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| | | | | |
| * | | | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| | | | | |
| * | | | | Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
| | | | | |
| * | | | | Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
| * | | | | Correct coqchk reductionGravatar Amin Timany2017-06-16
| | | | | |
| * | | | | Disable debug printingGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | Fix a mistake in record declaration
| * | | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| | | | | |
| * | | | | Fix bugsGravatar Amin Timany2017-06-16
|/ / / / /
| | | | * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| | | | |\
| | | | * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | | | |\ \
| | | | * \ \ Merge PR#752: Adding a test case as requested in bug 5205.Gravatar Maxime Dénès2017-06-15
| | | | |\ \ \
| | | | * \ \ \ Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Maxime Dénès2017-06-15
| | | | |\ \ \ \
* | | | | \ \ \ \ Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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)
* | | | | | | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | Remove dependency on -compat flag in coq_makefile test suite.Gravatar Maxime Dénès2017-06-15
| |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sorting for the dependency order option.
* | | | | | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
| | * | | | | | | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR#757: Better sectioning on travis log printing in test-suiteGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 15:09:59 +0000