aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\
* \ Merge PR #873: New strategy based on open scopes for deciding which notation ↵Gravatar Maxime Dénès2017-12-07
|\ \ | | | | | | | | | to use among several of them
* \ \ Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \
* \ \ \ Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Gravatar Maxime Dénès2017-12-05
|\ \ \ \
* \ \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6210: More complete not-fully-applied error messages, #6145Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \
| | | * | | | Adding a test for #6304 (bug with fix in notations).Gravatar Hugo Herbelin2017-12-03
| |_|/ / / / |/| | | | |
| | | * | | Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Regularly declared for for polymorphic constants - Declared globally for monomorphic constants. E.g mono@{i} := Type@{i} is printed as mono@{mono.i} := Type@{mono.i}. There can be a name clash if there's a module and a constant of the same name. It is detected and is an error if the constant is first but is not detected and the name for the constant not registered (??) if the constant comes second. Accept VarRef when registering universe binders Fix two problems found by Gaëtan where binders were not registered properly Simplify API substantially by not passing around a substructure of an already carrier-around structure in interpretation/declaration code of constants and proofs Fix an issue of the stronger restrict universe context + no evd leak This is uncovered by not having an evd leak in interp_definition, and the stronger restrict_universe_context. This patch could be backported to 8.7, it could also be triggered by the previous restrict_context I think.
| | | * | | Tests for global universe declarationsGravatar Matthieu Sozeau2017-12-01
| | | | | |
| | | * | | Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* | | | | 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).
| | | | * | | | more complete not-fully-applied error messages, #6145Gravatar Paul Steckler2017-11-28
| | | | | | | |
| | * | | | | | 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
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | |
| | | | | | * | Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | See discussion on coq-club starting on 23 August 2016. An open question: what priority to give to "abbreviations"?
| | | | | | * | Pre-isolating a notation test to avoid interferences.Gravatar Hugo Herbelin2017-11-27
| |_|_|_|_|/ / |/| | | | | |
* | | | | | | 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).
| | | | | | * Printing again "intros **" as "intros" by default.Gravatar Hugo Herbelin2017-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible).
| | | | | | * Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-24
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | Was broken since 8.6.
* | | | | | 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)
| | | | | | * allow whitespace around infix opGravatar Paul Steckler2017-11-22
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 17:25:27 +0000