aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
AgeCommit message (Collapse)Author
2018-11-16Add test for Include in -quick modeGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact.
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
With camlp4 this file was not created but now that we use mlg it has appeared.
2018-10-19Porting the test-suite to coqpp.Pierre-Marie Pédrot
2018-10-11[dune] [test-suite] Support for running the test suite with Dune.Emilio Jesus Gallego Arias
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert
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-07add test for #7595Ralf Jung
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gaëtan Gilbert
symlink from repo
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
Fixes #7065
2018-05-11Fix non-portable shebang in test-suite.Théo Zimmermann
2018-05-09test for coqc -oEnrico Tassi
2018-04-05Improve shell scriptszapashcanon
2017-09-13Adding a test for utf8 characters in directory names.Hugo Herbelin
2017-07-20Remove trailing CR before diff in output and misc tests.Maxime Dénès
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-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2016-07-04test-suite: test checking of libraries checksum.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19test suite update after r14808pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-25Add a test for sorting all universes of stdlibglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
coqdep since it is now deterministic (later -R's overwriting former ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-26Fixing xml theory file export (was not consistent with coqdoc fileherbelin
naming heuristic). Added a corresponding test. Note: maybe should the generated .v file for exporting the theory be made of a valid ident if ever coqdoc eventually follows coq convention: currently it has name foo.theory.v which is not coqc-compilable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12543 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:35:09 +0000