Merge pull request #33 from coq-community/compat-8.20 #47
Annotations
10 warnings
|
ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
|
|
tutorial_inductive_co_inductive_types/SRC/RecTutorial.v#L2
Using Vector.t is known to be technically difficult, see
|
|
ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
|
|
ch14_fundations_of_inductive_types/SRC/chap14.v#L86
Automatically putting type_name in Prop even though it was declared
|
|
ch14_fundations_of_inductive_types/SRC/triangular_dep.v#L1
Using Vector.t is known to be technically difficult, see
|
|
ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to
|
|
ch6_inductive_data/SRC/vectorsbis.v#L1
Using Vector.t is known to be technically difficult, see
|
|
ch6_inductive_data/SRC/vectors.v#L1
Using Vector.t is known to be technically difficult, see
|
|
ch8_inductive_predicates/SRC/chap8.v#L134
Using Vector.t is known to be technically difficult, see
|
|
ch8_inductive_predicates/SRC/JMeqSolution.v#L1
Using Vector.t is known to be technically difficult, see
|
The logs for this run have expired and are no longer available.
Loading