aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
(in case of side effects) Also: Fix #4781 Fix #4496
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵Pierre-Marie Pédrot
in right-hand side
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim).
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Restrict body universes in delayed mode.Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
You can tell which it is from the `@{}` if you really care, and seeing `Monomorphic List (A:Type)` with no indication that `Monomorphic` is about universes can confuse people.
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵Emilio Jesus Gallego Arias
(fix #9204)
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-13Merge PR #9117: Accept argument names for extra arguments with "extra scopes"Matthieu Sozeau
2018-12-13Merge PR #9032: checker: check inductive types by roundtrip through the kernel.Pierre-Marie Pédrot
2018-12-13Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵Pierre-Marie Pédrot
pattern variables
2018-12-13[test] for join when error resiliency on and async-proofs offEnrico Tassi
2018-12-13[test] for #9204Enrico Tassi
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
The checks were unnecessarily restrictive (since names can be used for documentation purposes), and the error message was a bit wrong (it mentioned a restriction on the explicit status of arguments).
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
2018-12-05Add test for #8951.Gaëtan Gilbert
Close #8951.
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position.
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though).
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore.
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016.
2018-12-04Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2018-11-28Add a couple more printing tests for byte/asciiJason Gross
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
We encode the conversion to bits with little-endian right-associative tuples to ensure that the head of the tuple (the `fst` element) is the least significant bit. We still enforce that the ordering of bits matches the order of the `bool`s in the `ascii` inductive type.
2018-11-28Speed up ByteJason Gross
We could move another ~ 1s from Init.Byte to Strings.Byte by moving `of_bits_to_bits` and `to_bits_of_bits`, but I figured it's probably not worth it. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------- 1m16.75s | Total | 1m21.45s || -0m04.70s | -5.77% ---------------------------------------------------------------------------------- 0m08.95s | Strings/Byte | 0m12.41s || -0m03.46s | -27.88% 0m07.24s | Byte | 0m08.76s || -0m01.51s | -17.35% 0m06.37s | plugins/setoid_ring/Ring_polynom | 0m06.24s || +0m00.12s | +2.08% 0m03.14s | Numbers/Integer/Abstract/ZBits | 0m03.20s || -0m00.06s | -1.87% 0m02.44s | ZArith/BinInt | 0m02.44s || +0m00.00s | +0.00% 0m02.24s | Numbers/Natural/Abstract/NBits | 0m02.20s || +0m00.04s | +1.81% 0m01.97s | Lists/List | 0m01.93s || +0m00.04s | +2.07% 0m01.85s | Numbers/NatInt/NZLog | 0m01.82s || +0m00.03s | +1.64% 0m01.78s | PArith/BinPos | 0m01.78s || +0m00.00s | +0.00% 0m01.74s | plugins/setoid_ring/InitialRing | 0m01.63s || +0m00.11s | +6.74% 0m01.73s | Strings/Ascii | 0m01.58s || +0m00.14s | +9.49% 0m01.39s | NArith/BinNat | 0m01.34s || +0m00.04s | +3.73% 0m01.32s | Numbers/NatInt/NZPow | 0m01.24s || +0m00.08s | +6.45% 0m01.22s | Numbers/NatInt/NZSqrt | 0m01.15s || +0m00.07s | +6.08% 0m01.11s | Arith/PeanoNat | 0m01.16s || -0m00.04s | -4.31% 0m01.10s | Numbers/Integer/Abstract/ZDivTrunc | 0m01.11s || -0m00.01s | -0.90% 0m01.02s | Specif | 0m01.04s || -0m00.02s | -1.92% 0m00.96s | Numbers/NatInt/NZMulOrder | 0m00.84s || +0m00.12s | +14.28% 0m00.95s | Numbers/Integer/Abstract/ZDivFloor | 0m00.97s || -0m00.02s | -2.06% 0m00.85s | plugins/setoid_ring/Ring_theory | 0m00.86s || -0m00.01s | -1.16% 0m00.82s | Structures/GenericMinMax | 0m00.85s || -0m00.03s | -3.52% 0m00.72s | Numbers/Integer/Abstract/ZLcm | 0m00.82s || -0m00.09s | -12.19% 0m00.69s | Numbers/NatInt/NZParity | 0m00.69s || +0m00.00s | +0.00% 0m00.68s | Numbers/NatInt/NZDiv | 0m00.71s || -0m00.02s | -4.22% 0m00.68s | Strings/String | 0m00.65s || +0m00.03s | +4.61% 0m00.64s | Numbers/Integer/Abstract/ZSgnAbs | 0m00.64s || +0m00.00s | +0.00% 0m00.64s | ZArith/Zeven | 0m00.48s || +0m00.16s | +33.33% 0m00.63s | ZArith/Zorder | 0m00.61s || +0m00.02s | +3.27% 0m00.57s | Numbers/Integer/Abstract/ZMulOrder | 0m00.67s || -0m00.10s | -14.92% 0m00.56s | Classes/Morphisms | 0m00.58s || -0m00.01s | -3.44% 0m00.55s | Numbers/NatInt/NZOrder | 0m00.51s || +0m00.04s | +7.84% 0m00.48s | ZArith/BinIntDef | 0m00.48s || +0m00.00s | +0.00% 0m00.46s | Classes/CMorphisms | 0m00.48s || -0m00.01s | -4.16% 0m00.46s | Numbers/Integer/Abstract/ZGcd | 0m00.46s || +0m00.00s | +0.00% 0m00.46s | Numbers/Natural/Abstract/NSub | 0m00.48s || -0m00.01s | -4.16% 0m00.45s | Logic | 0m00.44s || +0m00.01s | +2.27% 0m00.45s | Numbers/Natural/Abstract/NGcd | 0m00.48s || -0m00.02s | -6.24% 0m00.42s | Numbers/Natural/Abstract/NLcm | 0m00.40s || +0m00.01s | +4.99% 0m00.42s | Structures/OrdersFacts | 0m00.48s || -0m00.06s | -12.50% 0m00.41s | ZArith/Zbool | 0m00.38s || +0m00.02s | +7.89% 0m00.38s | Numbers/Integer/Abstract/ZPow | 0m00.34s || +0m00.03s | +11.76% 0m00.36s | Bool/Bool | 0m00.36s || +0m00.00s | +0.00% 0m00.36s | Numbers/NatInt/NZGcd | 0m00.35s || +0m00.01s | +2.85% 0m00.36s | ZArith/ZArith_dec | 0m00.38s || -0m00.02s | -5.26% 0m00.34s | Numbers/Integer/Abstract/ZAdd | 0m00.33s || +0m00.01s | +3.03% 0m00.34s | PArith/Pnat | 0m00.31s || +0m00.03s | +9.67% 0m00.32s | Numbers/Natural/Abstract/NOrder | 0m00.32s || +0m00.00s | +0.00% 0m00.32s | PArith/BinPosDef | 0m00.31s || +0m00.01s | +3.22% 0m00.32s | ZArith/Zcompare | 0m00.28s || +0m00.03s | +14.28% 0m00.30s | Classes/RelationClasses | 0m00.29s || +0m00.01s | +3.44% 0m00.30s | NArith/Nnat | 0m00.30s || +0m00.00s | +0.00% 0m00.29s | Numbers/Natural/Abstract/NAxioms | 0m00.26s || +0m00.02s | +11.53% 0m00.28s | Numbers/Integer/Abstract/ZAddOrder | 0m00.28s || +0m00.00s | +0.00% 0m00.28s | Structures/Orders | 0m00.30s || -0m00.01s | -6.66% 0m00.27s | Numbers/Integer/Abstract/ZAxioms | 0m00.23s || +0m00.04s | +17.39% 0m00.27s | Numbers/NatInt/NZAxioms | 0m00.26s || +0m00.01s | +3.84% 0m00.26s | Numbers/Integer/Abstract/ZMaxMin | 0m00.25s || +0m00.01s | +4.00% 0m00.26s | Numbers/NatInt/NZAdd | 0m00.28s || -0m00.02s | -7.14% 0m00.26s | Numbers/Natural/Abstract/NMaxMin | 0m00.24s || +0m00.02s | +8.33% 0m00.26s | Numbers/Natural/Abstract/NParity | 0m00.31s || -0m00.04s | -16.12% 0m00.26s | plugins/setoid_ring/ArithRing | 0m00.22s || +0m00.04s | +18.18% 0m00.26s | plugins/setoid_ring/Ring_tac | 0m00.24s || +0m00.02s | +8.33% 0m00.25s | Logic/Decidable | 0m00.26s || -0m00.01s | -3.84% 0m00.25s | Structures/OrdersTac | 0m00.25s || +0m00.00s | +0.00% 0m00.24s | Classes/Equivalence | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | Datatypes | 0m00.27s || -0m00.03s | -11.11% 0m00.24s | Numbers/NatInt/NZMul | 0m00.25s || -0m00.01s | -4.00% 0m00.24s | plugins/setoid_ring/Ring | 0m00.20s || +0m00.03s | +19.99% 0m00.23s | Numbers/NatInt/NZAddOrder | 0m00.33s || -0m00.10s | -30.30% 0m00.23s | Numbers/Natural/Abstract/NAdd | 0m00.17s || +0m00.06s | +35.29% 0m00.22s | Arith/Compare_dec | 0m00.22s || +0m00.00s | +0.00% 0m00.22s | Classes/CRelationClasses | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | Logic/EqdepFacts | 0m00.19s || +0m00.03s | +15.78% 0m00.22s | NArith/BinNatDef | 0m00.25s || -0m00.03s | -12.00% 0m00.22s | plugins/setoid_ring/Ring_base | 0m00.23s || -0m00.01s | -4.34% 0m00.21s | Arith/Arith | 0m00.19s || +0m00.01s | +10.52% 0m00.21s | Numbers/Natural/Abstract/NDiv | 0m00.19s || +0m00.01s | +10.52% 0m00.20s | Numbers/Integer/Abstract/ZProperties | 0m00.23s || -0m00.03s | -13.04% 0m00.20s | Relations/Relation_Operators | 0m00.17s || +0m00.03s | +17.64% 0m00.19s | Arith/Between | 0m00.22s || -0m00.03s | -13.63% 0m00.18s | Arith/Wf_nat | 0m00.24s || -0m00.06s | -25.00% 0m00.17s | Arith/Plus | 0m00.16s || +0m00.01s | +6.25% 0m00.17s | Nat | 0m00.18s || -0m00.00s | -5.55% 0m00.17s | Numbers/Natural/Abstract/NProperties | 0m00.22s || -0m00.04s | -22.72% 0m00.17s | Relations/Relation_Definitions | 0m00.08s || +0m00.09s | +112.50% 0m00.16s | Numbers/Integer/Abstract/ZLt | 0m00.16s || +0m00.00s | +0.00% 0m00.16s | Numbers/Natural/Abstract/NBase | 0m00.19s || -0m00.03s | -15.78% 0m00.16s | Numbers/Natural/Abstract/NPow | 0m00.15s || +0m00.01s | +6.66% 0m00.15s | Classes/Morphisms_Prop | 0m00.18s || -0m00.03s | -16.66% 0m00.14s | Arith/Mult | 0m00.12s || +0m00.02s | +16.66% 0m00.14s | Arith/Peano_dec | 0m00.16s || -0m00.01s | -12.49% 0m00.14s | Numbers/NatInt/NZBase | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Numbers/Natural/Abstract/NMulOrder | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | Relations/Operators_Properties | 0m00.13s || +0m00.01s | +7.69% 0m00.14s | plugins/setoid_ring/BinList | 0m00.16s || -0m00.01s | -12.49% 0m00.13s | Arith/EqNat | 0m00.18s || -0m00.04s | -27.77% 0m00.13s | Structures/Equalities | 0m00.17s || -0m00.04s | -23.52% 0m00.12s | Arith/Lt | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Arith/Minus | 0m00.13s || -0m00.01s | -7.69% 0m00.12s | Decimal | 0m00.16s || -0m00.04s | -25.00% 0m00.12s | Numbers/Integer/Abstract/ZBase | 0m00.09s || +0m00.03s | +33.33% 0m00.12s | Numbers/Integer/Abstract/ZMul | 0m00.12s || +0m00.00s | +0.00% 0m00.12s | Numbers/Integer/Abstract/ZParity | 0m00.11s || +0m00.00s | +9.09% 0m00.12s | Numbers/Natural/Abstract/NAddOrder | 0m00.12s || +0m00.00s | +0.00% 0m00.11s | Arith/Factorial | 0m00.11s || +0m00.00s | +0.00% 0m00.11s | Lists/ListTactics | 0m00.13s || -0m00.02s | -15.38% 0m00.11s | Logic/Eqdep_dec | 0m00.12s || -0m00.00s | -8.33% 0m00.11s | Numbers/Natural/Abstract/NLog | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Peano | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Program/Basics | 0m00.07s || +0m00.03s | +57.14% 0m00.10s | Arith/Gt | 0m00.13s || -0m00.03s | -23.07% 0m00.10s | Bool/Sumbool | 0m00.10s || +0m00.00s | +0.00% 0m00.10s | Numbers/Natural/Abstract/NSqrt | 0m00.12s || -0m00.01s | -16.66% 0m00.10s | Wf | 0m00.11s || -0m00.00s | -9.09% 0m00.09s | Arith/Arith_base | 0m00.09s || +0m00.00s | +0.00% 0m00.09s | Logic_Type | 0m00.08s || +0m00.00s | +12.49% 0m00.08s | Arith/Le | 0m00.11s || -0m00.03s | -27.27% 0m00.08s | Numbers/BinNums | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Numbers/NatInt/NZBits | 0m00.12s || -0m00.03s | -33.33% 0m00.08s | Numbers/NatInt/NZProperties | 0m00.09s || -0m00.00s | -11.11% 0m00.08s | Program/Tactics | 0m00.08s || +0m00.00s | +0.00% 0m00.07s | Tactics | 0m00.10s || -0m00.03s | -30.00% 0m00.06s | Classes/SetoidTactics | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Numbers/NumPrelude | 0m00.06s || +0m00.00s | +0.00% 0m00.05s | Classes/Init | 0m00.04s || +0m00.01s | +25.00% 0m00.05s | Prelude | 0m00.09s || -0m00.03s | -44.44% 0m00.05s | Setoids/Setoid | 0m00.08s || -0m00.03s | -37.50% 0m00.04s | Relations/Relations | 0m00.04s || +0m00.00s | +0.00% 0m00.04s | Tauto | 0m00.09s || -0m00.05s | -55.55% 0m00.02s | Notations | 0m00.04s || -0m00.02s | -50.00%
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
Users can now register string notations for custom inductives. Much of the code and documentation was copied from numeral notations. I chose to use a 256-constructor inductive for primitive string syntax because (a) it is easy to convert between character codes and constructors, and (b) it is more efficient than the existing `ascii` type. Some choices about proofs of the new `byte` type were made based on efficiency. For example, https://github.com/coq/coq/issues/8517 means that we cannot simply use `Scheme Equality` for this type, and I have taken some care to ensure that the proofs of decidable equality and conversion are fast. (Unfortunately, the `Init/Byte.v` file is the slowest one in the prelude (it takes a couple of seconds to build), and I'm not sure where the slowness is.) In String.v, some uses of `0` as a `nat` were replaced by `O`, because the file initially refused to check interactively otherwise (it complained that `0` could not be interpreted in `string_scope` before loading `Coq.Strings.String`). There is unfortunately a decent amount of code duplication between numeral notations and string notations. I have not put too much thought into chosing names; most names have been chosen to be similar to numeral notations, though I chose the name `byte` from https://github.com/coq/coq/issues/8483#issuecomment-421671785. Unfortunately, this feature does not support declaring string syntax for `list ascii`, unless that type is wrapped in a record or other inductive type. This is not a fundamental limitation; it should be relatively easy for someone who knows the API of the reduction machinery in Coq to extend both this and numeral notations to support any type whose hnf starts with an inductive type. (The reason for needing an inductive type to bottom out at is that this is how the plugin determines what constructors are the entry points for printing the given notation. However, see also https://github.com/coq/coq/issues/8964 for complications that are more likely to arise if inductive type families are supported.) N.B. I generated the long lists of constructors for the `byte` type with short python scripts. Closes #8853
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-28Merge PR #9089: Fix #9076 (warning appears when running test suite)Emilio Jesus Gallego Arias
2018-11-27Fix #9076 (warning appears when running test suite)Maxime Dénès
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
When making a universe a variable we iterate through the universes we're equal to and if we find one we update the substitution accordingly. NB: The bug called make_flexible_variable on Top.15 and ~~~ {Top.15 Top.14} |= Top.11 < Top.6 Top.14 < Top.5 Top.11 = Top.15 ALGEBRAIC UNIVERSES:{Top.17 Top.16} UNDEFINED UNIVERSES:Top.17 := Top.14+1 Top.16 := Top.14+1 WEAK CONSTRAINTS: ~~~ so now we would add [Top.15 := Top.11].
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:20:44 +0000