Fix test-suite due to changes in 8.18 #2594
mattam82Annotations
20 warnings
|
build (8.18, 4.14-flambda, opam)
Tactic elimtype is deprecated since 8.18. Use [elim] instead.
|
|
build (8.18, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
|
|
build (8.18, 4.14-flambda, opam)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
|
|
build (8.18, 4.14-flambda, opam)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, opam)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, opam)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, opam)
Huctx' is declared opaque (Qed) but this is not fully respected
|
|
build (8.18, 4.14-flambda, opam)
HC' is declared opaque (Qed) but this is not fully respected inside
|
|
build (8.18, 4.14-flambda, opam)
HG' is declared opaque (Qed) but this is not fully respected inside
|
|
build (8.18, 4.14-flambda, opam)
Argument typing_size was previously inferred to be in
|
|
build (8.18, 4.14-flambda, local)
Tactic elimtype is deprecated since 8.18. Use [elim] instead.
|
|
build (8.18, 4.14-flambda, local)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
|
|
build (8.18, 4.14-flambda, local)
Tactic Notation revert dependent (hyp) is deprecated since 8.18.
|
|
build (8.18, 4.14-flambda, local)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, local)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, local)
Variable na does not occur in the right-hand side. The notation will
|
|
build (8.18, 4.14-flambda, local)
Huctx' is declared opaque (Qed) but this is not fully respected
|
|
build (8.18, 4.14-flambda, local)
HC' is declared opaque (Qed) but this is not fully respected inside
|
|
build (8.18, 4.14-flambda, local)
HG' is declared opaque (Qed) but this is not fully respected inside
|
|
build (8.18, 4.14-flambda, local)
Argument typing_size was previously inferred to be in
|