aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
This allows to know which global references whose basename may be unexpectedly caught need to be qualified. Note: the alternative strategy, which is sometimes used, of renaming the binding variables so as to avoid collisions with the basename of a global reference is somehow less nice.
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
Reviewed-by: gares
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named ↵coqbot-app[bot]
variables. Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: SkySkimmer
2020-11-16Fix incorrect name refreshing when interning a generalized binderGaëtan Gilbert
Fix #13249
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context ↵coqbot-app[bot]
of the definition of the metas Reviewed-by: mattam82
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part ↵coqbot-app[bot]
of unification Reviewed-by: mattam82
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a ↵Pierre-Marie Pédrot
reference. Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
It remains to accept resolving Type(u)<=Prop for u arbitrary sort variable.
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
See 742ef62fe8050a6865d06bd644e30cbec0e7eb02 Fix #13366 Fix #9809
2020-11-16Finish fixing setoid rewrite under anonymous lambdas (hopefully)Gaëtan Gilbert
Fix #13246 Not sure if this is the right thing to do, but it seems to work.
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
Fix #13300
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ↵coqbot-app[bot]
sort elimination constraints Reviewed-by: gares
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
This makes it so that we have an application `h a b` with both `a` and `b` unbound, `a` is the one that is reported (parent commit with my current compiler setup reports `b` first, and the code does not define which it should be). Ideally we would report both but that requires more code.
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
This is consistent with the syntax of Notation and is (IMO) clearer.
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block ↵Li-yao Xia
verbatim from inline verbatim Reviewed-by: Lysxia
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation ↵Hugo Herbelin
(solve_simple_eqn). The bug was that an assumption could be interpreted as a local definition and wrongly expanded. It triggered rarely because it involved mixing let-ins and local assumptions + imitation under binders.
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an ↵coqbot-app[bot]
error, not an anomaly Reviewed-by: ejgallego
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a ↵coqbot-app[bot]
handler in NotFoundInstance Reviewed-by: ejgallego
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
Fix #6042 Also introduce a deprecated compat option
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
This allows the following to interpret "0" in the expected scope: Notation "0" := true : bool_scope. Axiom f : bool -> bool -> nat. Record R := { p : bool -> nat }. Check (@f 0) 0. Check fun r => r.(@p) 0.
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not ↵Pierre-Marie Pédrot
a keyword. Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
This does not affect the rendering but gives better structured html/tex files.
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
We clarify that there are two kinds of verbatim: inline and block. We add a test testing verbatim and others. Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
Fixes #13266 (see #12675, 8641cb7385).
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
In Evar := C[Meta] problems of unification.ml, and C[ ] contains binders, Meta was wrongly considered by pose_all_metas_as_evars as under these binders (while Metas are always defined in the initial context of the unification problem).
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
Fix #13348
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
Fix #13354 This change is very specific to array, but should not be a significant obstacle to generalization of the feature to eg axioms if we want to later.
2020-11-12Test case for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
in addition to having them as artefacts
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
I left the other test as a v file since it might become relevant when the corresponding Qed bug is fixed.
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
Polymorphic side-effects generated in monomorphic mode would be counted towards trusted subcomponents. This would allow to make ill-typed terms pass as legitimate by mimicking the shape of the inlining of monomorphic side-effects in such a proof.
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
(for runs outside dune, ie "make -C test-suite unit-tests" rather than "dune build @runtest") Fix #13333
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
Fixes #13320 . Trivial programming error, actually this is handled better in a further refactoring branch not submitted due to the long time the whole rework took.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 21:13:59 +0000