aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ↵Maxime Dénès
to use among several of them
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c].
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
- 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.
2017-12-01Tests for global universe declarationsMatthieu Sozeau
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
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
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Maxime Dénès
#3125)
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵Maxime Dénès
instance.
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵Maxime Dénès
of levels
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
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).
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Maxime Dénès
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016. An open question: what priority to give to "abbreviations"?
2017-11-27Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2017-11-27Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵Maxime Dénès
subdirectory.
2017-11-27Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsMaxime Dénès
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
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).
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
Also nicer error when the constraints are impossible.
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-25Make restrict_universe_context stronger.Gaëtan Gilbert
This fixes BZ#5717. Also add a test and fix a changed test.
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
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.
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Fix defining non primitive projections with abstracted universes.Gaëtan Gilbert
I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly.
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
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).
2017-11-24Printing again "intros **" as "intros" by default.Hugo Herbelin
The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible).
2017-11-24Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
Was broken since 8.6.
2017-11-24Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingMaxime Dénès
2017-11-24Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionMaxime Dénès
2017-11-24coq_makefile tests: build in easily removed temporary subdirectory.Gaëtan Gilbert
This allows us to avoid doing git clean.
2017-11-24Fixing failing mkdir in test-suite for coq-makefile.Hugo Herbelin
Calling the test a second time after a make clean was failing due to an existing "src" directory left by the first call.
2017-11-23Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Maxime Dénès
separator
2017-11-23Merge PR #6203: Fix universe polymorphic Program obligations.Maxime Dénès
2017-11-23Recognizing Z in romega up to conversion.Hugo Herbelin
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
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.
2017-11-23Fixing a 8.7 regression of ring_simplify in ArithRing.Hugo Herbelin
With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
2017-11-23Merge PR #6123: Nix fileMaxime Dénès
2017-11-23Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:23:31 +0000