Prepare the package for coq 8.20 (silence the tests, update meta.yml and

configure.ac)

configure.ac

@@ -10,7 +10,7 @@
 # will set several variables: (see AC_SUBST at the end of this file)
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-AC_INIT(coq-dpdgraph,1.0)
+AC_INIT(coq-dpdgraph,1.0-8.20)
 AC_MSG_NOTICE(AC_PACKAGE_NAME version AC_PACKAGE_VERSION)
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

meta.yml

@@ -6,7 +6,7 @@ organization: coq-community
 community: true
 action: true
 plugin: true
-branch: 'coq-master'
+branch: 'coq-v8.20'
 
 synopsis: >-
   Compute dependencies between Coq objects (definitions, theorems) and produce graphs
@@ -29,15 +29,15 @@ maintainers:
 
 opam-file-maintainer: [email protected]
 
-opam-file-version: dev
+opam-file-version: 8.20.dev
 
 license:
   fullname: GNU Lesser General Public License v2.1
   identifier: LGPL-2.1-only
 
 supported_coq_versions:
-  text: master (use the corresponding branch or release for other Coq versions)
-  opam: '{= "dev"}'
+  text: 8.20 (use the corresponding branch or release for other Coq versions)
+  opam: '{>= "8.20" & < "8.21~"}'
 
 supported_ocaml_versions:
     text: 4.05.0 or later
@@ -55,7 +55,7 @@ dependencies:
     [OCamlgraph](https://github.com/backtracking/ocamlgraph)
 
 tested_coq_opam_versions:
-- version: dev
+- version: 8.20
 
 namespace: dpdgraph
 

tests/Morph_rw.dot.oracle

@@ -14,19 +14,19 @@ Morph_Fequiv_refl [label="Fequiv_refl", URL=<Morph.html#Fequiv_refl>, fillcolor=
 Morph_Fequiv_sym [label="Fequiv_sym", URL=<Morph.html#Fequiv_sym>, fillcolor="#FFB57F"] ;
 RelationClasses_Equivalence [label="Equivalence", URL=<RelationClasses.html#Equivalence>, fillcolor="#E2CDFA"] ;
 RelationClasses_Build_Equivalence [label="Build_Equivalence", URL=<RelationClasses.html#Build_Equivalence>, fillcolor="#7FAAFF"] ;
+RelationClasses_Symmetric [label="Symmetric", URL=<RelationClasses.html#Symmetric>, fillcolor="#F070D1"] ;
 RelationClasses_Reflexive [label="Reflexive", URL=<RelationClasses.html#Reflexive>, fillcolor="#F070D1"] ;
 Relation_Definitions_relation [label="relation", URL=<Relation_Definitions.html#relation>, fillcolor="#F070D1"] ;
 RelationClasses_Transitive [label="Transitive", URL=<RelationClasses.html#Transitive>, fillcolor="#F070D1"] ;
-RelationClasses_Symmetric [label="Symmetric", URL=<RelationClasses.html#Symmetric>, fillcolor="#F070D1"] ;
 RelationClasses_Equivalence_Transitive [label="Equivalence_Transitive", URL=<RelationClasses.html#Equivalence_Transitive>, fillcolor="#7FFFD4"] ;
 RelationClasses_Equivalence_Symmetric [label="Equivalence_Symmetric", URL=<RelationClasses.html#Equivalence_Symmetric>, fillcolor="#7FFFD4"] ;
 RelationClasses_PER [label="PER", URL=<RelationClasses.html#PER>, fillcolor="#E2CDFA"] ;
 RelationClasses_Build_PER [label="Build_PER", URL=<RelationClasses.html#Build_PER>, fillcolor="#7FAAFF"] ;
 Morphisms_Proper [label="Proper", URL=<Morphisms.html#Proper>, fillcolor="#F070D1"] ;
 Morphisms_respectful [label="respectful", URL=<Morphisms.html#respectful>, fillcolor="#F070D1"] ;
-Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 [label="trans_sym_co_inv_impl_morphism_obligation_1", URL=<Morphisms.html#trans_sym_co_inv_impl_morphism_obligation_1>, fillcolor="#7FFFD4"] ;
 Basics_flip [label="flip", URL=<Basics.html#flip>, fillcolor="#F070D1"] ;
 Basics_impl [label="impl", URL=<Basics.html#impl>, fillcolor="#F070D1"] ;
+Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 [label="trans_sym_co_inv_impl_morphism_obligation_1", URL=<Morphisms.html#trans_sym_co_inv_impl_morphism_obligation_1>, fillcolor="#7FFFD4"] ;
 RelationClasses_PER_Symmetric [label="PER_Symmetric", URL=<RelationClasses.html#PER_Symmetric>, fillcolor="#7FFFD4"] ;
 RelationClasses_symmetry [label="symmetry", URL=<RelationClasses.html#symmetry>, fillcolor="#7FFFD4"] ;
 RelationClasses_PER_Transitive [label="PER_Transitive", URL=<RelationClasses.html#PER_Transitive>, fillcolor="#7FFFD4"] ;
@@ -55,21 +55,21 @@ RelationClasses_transitivity [label="transitivity", URL=<RelationClasses.html#tr
   Morph_Fequiv_trans -> Morph_Fequiv [] ;
   Morph_Fequiv_refl -> Morph_Fequiv [] ;
   Morph_Fequiv_sym -> Morph_Fequiv [] ;
+  RelationClasses_Equivalence -> RelationClasses_Symmetric [] ;
   RelationClasses_Equivalence -> RelationClasses_Reflexive [] ;
   RelationClasses_Equivalence -> RelationClasses_Transitive [] ;
-  RelationClasses_Equivalence -> RelationClasses_Symmetric [] ;
+  RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ;
   RelationClasses_Build_Equivalence -> RelationClasses_Reflexive [] ;
   RelationClasses_Build_Equivalence -> RelationClasses_Transitive [] ;
-  RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ;
+  RelationClasses_Symmetric -> Relation_Definitions_relation [] ;
   RelationClasses_Reflexive -> Relation_Definitions_relation [] ;
   RelationClasses_Transitive -> Relation_Definitions_relation [] ;
-  RelationClasses_Symmetric -> Relation_Definitions_relation [] ;
   RelationClasses_Equivalence_Transitive -> RelationClasses_Equivalence [] ;
   RelationClasses_Equivalence_Symmetric -> RelationClasses_Equivalence [] ;
-  RelationClasses_PER -> RelationClasses_Transitive [] ;
   RelationClasses_PER -> RelationClasses_Symmetric [] ;
-  RelationClasses_Build_PER -> RelationClasses_Transitive [] ;
+  RelationClasses_PER -> RelationClasses_Transitive [] ;
   RelationClasses_Build_PER -> RelationClasses_Symmetric [] ;
+  RelationClasses_Build_PER -> RelationClasses_Transitive [] ;
   Morphisms_Proper -> Relation_Definitions_relation [] ;
   Morphisms_respectful -> Relation_Definitions_relation [] ;
   Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Morphisms_respectful [] ;
@@ -86,7 +86,7 @@ RelationClasses_transitivity [label="transitivity", URL=<RelationClasses.html#tr
 subgraph cluster_Basics { label="Basics"; fillcolor="#FFFFC3"; labeljust=l; style=filled 
 Basics_impl; Basics_flip; };
 subgraph cluster_RelationClasses { label="RelationClasses"; fillcolor="#FFFFC3"; labeljust=l; style=filled 
-RelationClasses_transitivity; RelationClasses_PER_Transitive; RelationClasses_symmetry; RelationClasses_PER_Symmetric; RelationClasses_Build_PER; RelationClasses_PER; RelationClasses_Equivalence_Symmetric; RelationClasses_Equivalence_Transitive; RelationClasses_Symmetric; RelationClasses_Transitive; RelationClasses_Reflexive; RelationClasses_Build_Equivalence; RelationClasses_Equivalence; RelationClasses_Equivalence_PER; };
+RelationClasses_transitivity; RelationClasses_PER_Transitive; RelationClasses_symmetry; RelationClasses_PER_Symmetric; RelationClasses_Build_PER; RelationClasses_PER; RelationClasses_Equivalence_Symmetric; RelationClasses_Equivalence_Transitive; RelationClasses_Transitive; RelationClasses_Reflexive; RelationClasses_Symmetric; RelationClasses_Build_Equivalence; RelationClasses_Equivalence; RelationClasses_Equivalence_PER; };
 subgraph cluster_Morphisms { label="Morphisms"; fillcolor="#FFFFC3"; labeljust=l; style=filled 
 Morphisms_trans_sym_co_inv_impl_morphism_obligation_1; Morphisms_respectful; Morphisms_Proper; Morphisms_trans_sym_co_inv_impl_morphism; };
 subgraph cluster_Relation_Definitions { label="Relation_Definitions"; fillcolor="#FFFFC3"; labeljust=l; style=filled 

tests/Morph_rw.dpd.oracle

@@ -12,17 +12,17 @@ N: 17 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ];
 N: 41 "PER_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
 N: 43 "PER_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
 N: 36 "Proper" [body=yes, kind=cnst, prop=no, path="Morphisms", ];
-N: 28 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
-N: 31 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
-N: 30 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
-N: 39 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ];
-N: 40 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ];
-N: 29 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ];
+N: 29 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
+N: 28 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
+N: 31 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
+N: 38 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ];
+N: 39 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ];
+N: 30 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ];
 N: 37 "respectful" [body=yes, kind=cnst, prop=no, path="Morphisms", ];
 N: 15 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ];
 N: 42 "symmetry" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
 N: 16 "trans_sym_co_inv_impl_morphism" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
-N: 38 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
+N: 40 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
 N: 44 "transitivity" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
 N: 26 "Equivalence" [kind=inductive, prop=no, path="RelationClasses", ];
 N: 34 "PER" [kind=inductive, prop=no, path="RelationClasses", ];
@@ -35,7 +35,7 @@ E: 15 19 [weight=5, ];
 E: 15 20 [weight=1, ];
 E: 15 21 [weight=8, ];
 E: 15 22 [weight=1, ];
-E: 16 29 [weight=3, ];
+E: 16 30 [weight=3, ];
 E: 16 34 [weight=3, ];
 E: 16 36 [weight=1, ];
 E: 16 37 [weight=1, ];
@@ -49,7 +49,7 @@ E: 17 36 [weight=1, ];
 E: 17 37 [weight=1, ];
 E: 19 18 [weight=2, ];
 E: 20 26 [weight=2, ];
-E: 20 29 [weight=2, ];
+E: 20 30 [weight=2, ];
 E: 20 32 [weight=1, ];
 E: 20 33 [weight=1, ];
 E: 20 34 [weight=1, ];
@@ -76,39 +76,39 @@ E: 27 28 [weight=1, ];
 E: 27 29 [weight=1, ];
 E: 27 30 [weight=1, ];
 E: 27 31 [weight=1, ];
-E: 28 29 [weight=2, ];
-E: 30 29 [weight=2, ];
-E: 31 29 [weight=2, ];
+E: 28 30 [weight=2, ];
+E: 29 30 [weight=2, ];
+E: 31 30 [weight=2, ];
 E: 32 26 [weight=3, ];
-E: 32 29 [weight=2, ];
 E: 32 30 [weight=2, ];
+E: 32 31 [weight=2, ];
 E: 33 26 [weight=3, ];
-E: 33 29 [weight=2, ];
-E: 33 31 [weight=2, ];
-E: 34 29 [weight=1, ];
+E: 33 28 [weight=2, ];
+E: 33 30 [weight=2, ];
+E: 34 28 [weight=1, ];
 E: 34 30 [weight=1, ];
 E: 34 31 [weight=1, ];
-E: 35 29 [weight=1, ];
+E: 35 28 [weight=1, ];
 E: 35 30 [weight=1, ];
 E: 35 31 [weight=1, ];
-E: 36 29 [weight=2, ];
-E: 37 29 [weight=5, ];
-E: 38 29 [weight=2, ];
-E: 38 34 [weight=2, ];
-E: 38 37 [weight=1, ];
-E: 38 39 [weight=1, ];
-E: 38 40 [weight=1, ];
-E: 38 41 [weight=1, ];
-E: 38 42 [weight=1, ];
-E: 38 43 [weight=1, ];
-E: 38 44 [weight=1, ];
-E: 41 29 [weight=2, ];
-E: 41 31 [weight=2, ];
+E: 36 30 [weight=2, ];
+E: 37 30 [weight=5, ];
+E: 40 30 [weight=2, ];
+E: 40 34 [weight=2, ];
+E: 40 37 [weight=1, ];
+E: 40 38 [weight=1, ];
+E: 40 39 [weight=1, ];
+E: 40 41 [weight=1, ];
+E: 40 42 [weight=1, ];
+E: 40 43 [weight=1, ];
+E: 40 44 [weight=1, ];
+E: 41 28 [weight=2, ];
+E: 41 30 [weight=2, ];
 E: 41 34 [weight=3, ];
-E: 42 29 [weight=2, ];
-E: 42 31 [weight=2, ];
-E: 43 29 [weight=2, ];
+E: 42 28 [weight=2, ];
+E: 42 30 [weight=2, ];
 E: 43 30 [weight=2, ];
+E: 43 31 [weight=2, ];
 E: 43 34 [weight=3, ];
-E: 44 29 [weight=2, ];
 E: 44 30 [weight=2, ];
+E: 44 31 [weight=2, ];

tests/PrimitiveProjections.v

@@ -3,6 +3,7 @@ Set Implicit Arguments.
 
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 
+Set Warnings "-notation-overridden".
 Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
 
 Definition bar := @projT1.

tests/Test.v

@@ -569,8 +569,8 @@ Section Elts.
     induction l as [|y l].
     simpl; intros; split; [destruct 1 | apply Nat.lt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
-    rewrite Heq; intuition auto with *.
-    pose (IHl x). intuition auto with *.
+    rewrite Heq; intuition auto with arith.
+    pose (IHl x). intuition auto with arith.
   Qed.
 
   Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.

tests/graph.dpd.oracle

@@ -888,7 +888,7 @@ E: 125 179 [weight=1, ];
 E: 125 181 [weight=3, ];
 E: 125 182 [weight=11, ];
 E: 125 183 [weight=14, ];
-E: 126 127 [weight=29, ];
+E: 126 127 [weight=33, ];
 E: 126 170 [weight=27, ];
 E: 126 179 [weight=1, ];
 E: 126 181 [weight=2, ];

tests/graph2.dot.oracle

@@ -4,11 +4,11 @@ digraph tests/graph2 {
 Test_Permutation_app_swap [label="Permutation_app_swap", URL=<Test.html#Permutation_app_swap>, peripheries=3, fillcolor="#7FFFD4"] ;
 Test_Permutation_sym [label="Permutation_sym", URL=<Test.html#Permutation_sym>, fillcolor="#7FFFD4"] ;
 Test_app_nil_end [label="app_nil_end", URL=<Test.html#app_nil_end>, fillcolor="#7FFFD4"] ;
-_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ;
-_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ;
 Test_app_comm_cons [label="app_comm_cons", URL=<Test.html#app_comm_cons>, fillcolor="#7FFFD4"] ;
 Test_Permutation_refl [label="Permutation_refl", URL=<Test.html#Permutation_refl>, fillcolor="#7FFFD4"] ;
 Test_list_ind [label="list_ind", URL=<Test.html#list_ind>, fillcolor="#7FFFD4"] ;
+_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ;
+_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ;
 Test_Permutation_trans [label="Permutation_trans", URL=<Test.html#Permutation_trans>, fillcolor="#7FFFD4"] ;
 Test_app [label="app", URL=<Test.html#app>, fillcolor="#F070D1"] ;
 Test_Permutation [label="Permutation", URL=<Test.html#Permutation>, fillcolor="#E2CDFA"] ;
@@ -18,29 +18,26 @@ Test_perm_swap [label="perm_swap", URL=<Test.html#perm_swap>, fillcolor="#7FAAFF
 Test_nil [label="nil", URL=<Test.html#nil>, fillcolor="#7FAAFF"] ;
 Test_cons [label="cons", URL=<Test.html#cons>, fillcolor="#7FAAFF"] ;
 Test_perm_trans [label="perm_trans", URL=<Test.html#perm_trans>, fillcolor="#7FAAFF"] ;
-Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
+_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
 _eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ;
 _eq_refl [label="eq_refl", URL=<.html#eq_refl>, fillcolor="#7FAAFF"] ;
-_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
+Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
 Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>, fillcolor="#7FFFD4"] ;
   Test_Permutation_app_swap -> Test_Permutation_sym [] ;
   Test_Permutation_app_swap -> Test_app_nil_end [] ;
-  Test_Permutation_app_swap -> _eq_ind_r [] ;
   Test_Permutation_app_swap -> Test_app_comm_cons [] ;
   Test_Permutation_app_swap -> Test_Permutation_refl [] ;
+  Test_Permutation_app_swap -> _eq_ind_r [] ;
   Test_Permutation_app_swap -> Test_Permutation_trans [] ;
   Test_Permutation_sym -> Test_perm_skip [] ;
   Test_Permutation_sym -> Test_perm_swap [] ;
   Test_Permutation_sym -> Test_perm_trans [] ;
   Test_Permutation_sym -> Test_perm_nil [] ;
   Test_Permutation_sym -> Test_Permutation_ind [] ;
-  Test_app_nil_end -> _eq_ind [] ;
   Test_app_nil_end -> Test_list_ind [] ;
+  Test_app_nil_end -> _eq_ind [] ;
   Test_app_nil_end -> Test_app [] ;
   Test_app_nil_end -> _eq_refl [] ;
-  _eq_ind -> _eq [] ;
-  _eq_ind_r -> _eq_ind [] ;
-  _eq_ind_r -> _eq_sym [] ;
   Test_app_comm_cons -> Test_app [] ;
   Test_app_comm_cons -> _eq [] ;
   Test_app_comm_cons -> _eq_refl [] ;
@@ -51,6 +48,9 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
   Test_list_ind -> Test_list [] ;
   Test_list_ind -> Test_nil [] ;
   Test_list_ind -> Test_cons [] ;
+  _eq_ind -> _eq [] ;
+  _eq_ind_r -> _eq_ind [] ;
+  _eq_ind_r -> _eq_sym [] ;
   Test_Permutation_trans -> Test_Permutation [] ;
   Test_Permutation_trans -> Test_perm_trans [] ;
   Test_app -> Test_list [] ;
@@ -67,11 +67,11 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
   Test_perm_trans -> Test_list [] ;
   Test_perm_trans -> Test_nil [] ;
   Test_perm_trans -> Test_cons [] ;
+  _eq_sym -> _eq [] ;
+  _eq_sym -> _eq_refl [] ;
   Test_perm_nil -> Test_list [] ;
   Test_perm_nil -> Test_nil [] ;
   Test_perm_nil -> Test_cons [] ;
-  _eq_sym -> _eq [] ;
-  _eq_sym -> _eq_refl [] ;
   Test_Permutation_ind -> Test_Permutation [] ;
 subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled 
 Test_Permutation_ind; Test_perm_nil; Test_perm_trans; Test_cons; Test_nil; Test_perm_swap; Test_perm_skip; Test_list; Test_Permutation; Test_app; Test_Permutation_trans; Test_list_ind; Test_Permutation_refl; Test_app_comm_cons; Test_app_nil_end; Test_Permutation_sym; Test_Permutation_app_swap; };