aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Gravatar Maxime Dénès2017-11-30
|\ | | | | | | #3125)
* \ Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵Gravatar Maxime Dénès2017-11-30
|\ \ | | | | | | | | | instance.
* \ \ Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵Gravatar Maxime Dénès2017-11-29
|\ \ \ | | | | | | | | | | | | of levels
| | | * In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).
| | * | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ / |/| |
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* \ \ \ Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Gravatar Maxime Dénès2017-11-28
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵Gravatar Maxime Dénès2017-11-27
|\ \ \ \ | | | | | | | | | | | | | | | subdirectory.
* \ \ \ \ Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsGravatar Maxime Dénès2017-11-27
|\ \ \ \ \
| | | | | * Fixing associativity registered for level 10.Gravatar Hugo Herbelin2017-11-27
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
| | | | * Restrict universe context when declaring constants in obligations.Gravatar Gaëtan Gilbert2017-11-25
| | | | |
| | | | * Fix #5347: unify declaration of axioms with and without bound univs.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
| | | | * Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | | | Also nicer error when the constraints are impossible.
| | | | * Forbid repeated names in universe binders.Gravatar Gaëtan Gilbert2017-11-25
| | | | |
| | | | * Universe binders survive sections, modules and compilation.Gravatar Gaëtan Gilbert2017-11-25
| | | | |
| | | | * Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
| | | | |
| | | | * Make restrict_universe_context stronger.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes BZ#5717. Also add a test and fix a changed test.
| | | | * In close_proof only check univ decls with the restricted context.Gravatar Gaëtan Gilbert2017-11-24
| | | | |
| | | | * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
| | | | * restrict_universe_context: do not prune named universes.Gravatar Gaëtan Gilbert2017-11-24
| | | | |
| | | | * Fix defining non primitive projections with abstracted universes.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly.
| | | | * Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
* | | | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingGravatar Maxime Dénès2017-11-24
|\ \ \ \
* \ \ \ \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \ \ \ \
| | | | * | coq_makefile tests: build in easily removed temporary subdirectory.Gravatar Gaëtan Gilbert2017-11-24
| |_|_|/ / |/| | | | | | | | | | | | | | This allows us to avoid doing git clean.
| | | | * Fixing failing mkdir in test-suite for coq-makefile.Gravatar Hugo Herbelin2017-11-24
| |_|_|/ |/| | | | | | | | | | | | | | | Calling the test a second time after a make clean was failing due to an existing "src" directory left by the first call.
* | | | Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Gravatar Maxime Dénès2017-11-23
|\ \ \ \ | | | | | | | | | | | | | | | separator
* \ \ \ \ Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \
| | | * | | Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | | | |
| | | * | | Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
| | | * | Fixing a 8.7 regression of ring_simplify in ArithRing.Gravatar Hugo Herbelin2017-11-23
| |_|/ / |/| | | | | | | | | | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
* | | | Merge PR #6123: Nix fileGravatar Maxime Dénès2017-11-23
|\ \ \ \
* \ \ \ \ Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \ \ \ \
| | | | | * Add test-suite tests for timing scriptsGravatar Jason Gross2017-11-22
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all *.log files, so we use *.log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per https://github.com/coq/coq/pull/6149#issuecomment-346410990)
| | | * | Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
* | | | | Merge PR #6178: Have the coq_makefile timing test-suite print moreGravatar Maxime Dénès2017-11-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| * | | | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | | | | | | | | | Was broken since 8.6.
| | | | | * Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
* | | | | Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | (clause "where" with implicit arguments)
* \ \ \ \ \ \ Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | unbound rel
| | | | | | * | Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|_|_|/ / |/| | | | | |
| | | | | * | Have the coq_makefile timing test-suite print moreGravatar Jason Gross2017-11-17
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
* | | | | | Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | local definitions)
* \ \ \ \ \ \ Merge PR #6104: Fixing encoding in coqdoc output tests.Gravatar Maxime Dénès2017-11-16
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | |
| | | | | * | Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | Fixes #6165.
| | | * | | Fix #5761: cbv on undefined evars under binders produces unbound relGravatar Gaëtan Gilbert2017-11-15
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
* | | | | Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Gravatar Maxime Dénès2017-11-15
|\ \ \ \ \
| | | * | | Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
| |_|/ / / |/| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 04:15:15 +0000