aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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
2017-11-22Add test-suite tests for timing scriptsJason Gross
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)
2017-11-22allow whitespace around infix opPaul Steckler
2017-11-22use OCaml criteria for infix ops, #6212Paul Steckler
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
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.
2017-11-21Merge PR #6178: Have the coq_makefile timing test-suite print moreMaxime Dénès
2017-11-21Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesMaxime Dénès
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
Was broken since 8.6.
2017-11-20Fixing factorization of recursive notations in the case of an atomic separator.Hugo Herbelin
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.
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Maxime Dénès
(clause "where" with implicit arguments)
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Maxime Dénès
unbound rel
2017-11-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-17Have the coq_makefile timing test-suite print moreJason Gross
This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
2017-11-16Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Maxime Dénès
local definitions)
2017-11-16Merge PR #6104: Fixing encoding in coqdoc output tests.Maxime Dénès
2017-11-15Fix regression in treating Defined as definedTej Chajed
Fixes #6165.
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
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.
2017-11-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
2017-11-15Fix test-suite.Robbert Krebbers
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
2017-11-13Fixing encoding in coqdoc output tests.Hugo Herbelin
The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 08:20:50 +0000