Skip to content
Docker CI

Merge pull request #33 from coq-community/compat-8.20 #47

Sign in to view logs

Merge pull request #33 from coq-community/compat-8.20

Merge pull request #33 from coq-community/compat-8.20 #47

Triggered via push July 24, 2024 16:38
@palmskogpalmskog
pushed 907f3da
master
Status Success
Total duration 2m 35s
Artifacts –

docker-action.yml

on: push
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

24 warnings
build (coqorg/coq:8.20): ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
build (coqorg/coq:8.20): tutorial_inductive_co_inductive_types/SRC/RecTutorial.v#L2
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.20): ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
build (coqorg/coq:8.20): ch14_fundations_of_inductive_types/SRC/chap14.v#L86
Automatically putting type_name in Prop even though it was declared
build (coqorg/coq:8.20): ch14_fundations_of_inductive_types/SRC/triangular_dep.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.20): ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to
build (coqorg/coq:8.20): ch6_inductive_data/SRC/vectorsbis.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.20): ch6_inductive_data/SRC/vectors.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.20): ch8_inductive_predicates/SRC/chap8.v#L134
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.20): ch8_inductive_predicates/SRC/JMeqSolution.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
build (coqorg/coq:dev): tutorial_inductive_co_inductive_types/SRC/RecTutorial.v#L2
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
build (coqorg/coq:dev): ch14_fundations_of_inductive_types/SRC/chap14.v#L86
Automatically putting type_name in Prop even though it was declared
build (coqorg/coq:dev): ch14_fundations_of_inductive_types/SRC/triangular_dep.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to
build (coqorg/coq:dev): ch6_inductive_data/SRC/vectorsbis.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch6_inductive_data/SRC/vectors.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch8_inductive_predicates/SRC/chap8.v#L134
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:dev): ch8_inductive_predicates/SRC/JMeqSolution.v#L1
Using Vector.t is known to be technically difficult, see
build (coqorg/coq:8.18): ch8_inductive_predicates/SRC/magaud.v#L34
nu_constant is declared opaque (Qed) but this is not fully respected
build (coqorg/coq:8.19): ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
build (coqorg/coq:8.19): ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
build (coqorg/coq:8.19): ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to