Skip to content

Commit

Permalink
Merge pull request #133 from coq-community/coq_19310
Browse files Browse the repository at this point in the history 
Adapt to coq/coq#19310
  • Loading branch information
@proux01
proux01 authored Sep 10, 2024
2 parents 83711f4 + 0459e94 commit 4904006
Show file tree
Hide file tree
Showing 5 changed files with 90 additions and 90 deletions.
16 changes: 8 additions & 8 deletions tests/Morph_rw.dot.oracle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"] ;
Expand Down Expand Up @@ -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_Build_Equivalence -> RelationClasses_Symmetric [] ;
RelationClasses_Equivalence -> RelationClasses_Symmetric [] ;
RelationClasses_Build_Equivalence -> RelationClasses_Reflexive [] ;
RelationClasses_Build_Equivalence -> RelationClasses_Transitive [] ;
RelationClasses_Symmetric -> Relation_Definitions_relation [] ;
RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ;
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_Symmetric [] ;
RelationClasses_PER -> RelationClasses_Transitive [] ;
RelationClasses_Build_PER -> RelationClasses_Symmetric [] ;
RelationClasses_PER -> RelationClasses_Symmetric [] ;
RelationClasses_Build_PER -> RelationClasses_Transitive [] ;
RelationClasses_Build_PER -> RelationClasses_Symmetric [] ;
Morphisms_Proper -> Relation_Definitions_relation [] ;
Morphisms_respectful -> Relation_Definitions_relation [] ;
Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Morphisms_respectful [] ;
Expand All @@ -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_Transitive; RelationClasses_Reflexive; RelationClasses_Symmetric; 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_Symmetric; RelationClasses_Transitive; RelationClasses_Reflexive; 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
Expand Down
68 changes: 34 additions & 34 deletions tests/Morph_rw.dpd.oracle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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: 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: 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: 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: 40 "trans_sym_co_inv_impl_morphism_obligation_1" [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: 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", ];
Expand All @@ -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 30 [weight=3, ];
E: 16 29 [weight=3, ];
E: 16 34 [weight=3, ];
E: 16 36 [weight=1, ];
E: 16 37 [weight=1, ];
Expand All @@ -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 30 [weight=2, ];
E: 20 29 [weight=2, ];
E: 20 32 [weight=1, ];
E: 20 33 [weight=1, ];
E: 20 34 [weight=1, ];
Expand All @@ -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 30 [weight=2, ];
E: 29 30 [weight=2, ];
E: 31 30 [weight=2, ];
E: 28 29 [weight=2, ];
E: 30 29 [weight=2, ];
E: 31 29 [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 28 [weight=2, ];
E: 33 30 [weight=2, ];
E: 34 28 [weight=1, ];
E: 33 29 [weight=2, ];
E: 33 31 [weight=2, ];
E: 34 29 [weight=1, ];
E: 34 30 [weight=1, ];
E: 34 31 [weight=1, ];
E: 35 28 [weight=1, ];
E: 35 29 [weight=1, ];
E: 35 30 [weight=1, ];
E: 35 31 [weight=1, ];
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: 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: 41 34 [weight=3, ];
E: 42 28 [weight=2, ];
E: 42 30 [weight=2, ];
E: 42 29 [weight=2, ];
E: 42 31 [weight=2, ];
E: 43 29 [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, ];
22 changes: 11 additions & 11 deletions tests/graph2.dot.oracle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"] ;
Expand All @@ -18,26 +18,29 @@ 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"] ;
_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
_eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ;
_eq_refl [label="eq_refl", URL=<.html#eq_refl>, 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"] ;
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 -> Test_list_ind [] ;
Test_app_nil_end -> _eq_ind [] ;
Test_app_nil_end -> Test_list_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 [] ;
Expand All @@ -48,9 +51,6 @@ 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 [] ;
Expand All @@ -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; };
Expand Down
70 changes: 35 additions & 35 deletions tests/graph2.dpd.oracle
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
N: 184 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 205 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 188 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 190 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 185 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 192 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 193 "app" [body=yes, kind=cnst, prop=no, path="Test", ];
N: 187 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 189 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 186 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 190 "eq_ind" [body=yes, kind=cnst, prop=yes, ];
N: 191 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ];
N: 201 "eq_sym" [body=yes, kind=cnst, prop=yes, ];
N: 189 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 187 "eq_ind" [body=yes, kind=cnst, prop=yes, ];
N: 188 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ];
N: 204 "eq_sym" [body=yes, kind=cnst, prop=yes, ];
N: 191 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 194 "Permutation" [kind=inductive, prop=no, path="Test", ];
N: 202 "eq" [kind=inductive, prop=no, ];
N: 195 "list" [kind=inductive, prop=no, path="Test", ];
N: 204 "perm_nil" [kind=construct, prop=yes, path="Test", ];
N: 201 "perm_nil" [kind=construct, prop=yes, path="Test", ];
N: 203 "eq_refl" [kind=construct, prop=yes, ];
N: 198 "nil" [kind=construct, prop=no, path="Test", ];
N: 196 "perm_skip" [kind=construct, prop=yes, path="Test", ];
Expand All @@ -22,11 +22,11 @@ N: 197 "perm_swap" [kind=construct, prop=yes, path="Test", ];
N: 200 "perm_trans" [kind=construct, prop=yes, path="Test", ];
E: 184 185 [weight=3, ];
E: 184 186 [weight=2, ];
E: 184 187 [weight=1, ];
E: 184 188 [weight=2, ];
E: 184 189 [weight=2, ];
E: 184 187 [weight=2, ];
E: 184 188 [weight=1, ];
E: 184 189 [weight=1, ];
E: 184 190 [weight=2, ];
E: 184 191 [weight=1, ];
E: 184 191 [weight=2, ];
E: 184 192 [weight=3, ];
E: 184 193 [weight=43, ];
E: 184 194 [weight=11, ];
Expand All @@ -40,33 +40,33 @@ E: 185 195 [weight=12, ];
E: 185 196 [weight=1, ];
E: 185 197 [weight=1, ];
E: 185 200 [weight=1, ];
E: 185 204 [weight=1, ];
E: 185 201 [weight=1, ];
E: 185 205 [weight=1, ];
E: 186 189 [weight=1, ];
E: 186 190 [weight=1, ];
E: 186 187 [weight=1, ];
E: 186 191 [weight=1, ];
E: 186 193 [weight=6, ];
E: 186 195 [weight=14, ];
E: 186 198 [weight=9, ];
E: 186 199 [weight=5, ];
E: 186 202 [weight=6, ];
E: 186 203 [weight=2, ];
E: 187 193 [weight=3, ];
E: 187 195 [weight=6, ];
E: 187 199 [weight=3, ];
E: 187 202 [weight=1, ];
E: 187 203 [weight=1, ];
E: 188 189 [weight=1, ];
E: 188 194 [weight=3, ];
E: 188 195 [weight=4, ];
E: 188 196 [weight=1, ];
E: 187 202 [weight=3, ];
E: 188 187 [weight=1, ];
E: 188 202 [weight=2, ];
E: 188 204 [weight=1, ];
E: 189 195 [weight=8, ];
E: 189 198 [weight=2, ];
E: 189 199 [weight=2, ];
E: 190 202 [weight=3, ];
E: 191 190 [weight=1, ];
E: 191 201 [weight=1, ];
E: 191 202 [weight=2, ];
E: 189 193 [weight=3, ];
E: 189 195 [weight=6, ];
E: 189 199 [weight=3, ];
E: 189 202 [weight=1, ];
E: 189 203 [weight=1, ];
E: 190 191 [weight=1, ];
E: 190 194 [weight=3, ];
E: 190 195 [weight=4, ];
E: 190 196 [weight=1, ];
E: 190 201 [weight=1, ];
E: 191 195 [weight=8, ];
E: 191 198 [weight=2, ];
E: 191 199 [weight=2, ];
E: 192 194 [weight=3, ];
E: 192 195 [weight=3, ];
E: 192 200 [weight=1, ];
Expand All @@ -84,11 +84,11 @@ E: 197 199 [weight=6, ];
E: 200 195 [weight=6, ];
E: 200 198 [weight=2, ];
E: 200 199 [weight=6, ];
E: 201 202 [weight=5, ];
E: 201 203 [weight=1, ];
E: 204 195 [weight=6, ];
E: 204 198 [weight=2, ];
E: 204 199 [weight=6, ];
E: 201 195 [weight=6, ];
E: 201 198 [weight=2, ];
E: 201 199 [weight=6, ];
E: 204 202 [weight=5, ];
E: 204 203 [weight=1, ];
E: 205 194 [weight=10, ];
E: 205 195 [weight=22, ];
E: 205 198 [weight=4, ];
Expand Down
4 changes: 2 additions & 2 deletions tests/search.oracle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,5 @@ Welcome to Coq
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Fetching opaque proofs from disk for dpdgraph.tests.Test
[cons(42) nil(6) perm_swap(1) perm_skip(3) list(18) Permutation(11) app(43)
Permutation_trans(3) eq_ind_r(1) eq_ind(2) list_ind(2) Permutation_refl(2)
app_comm_cons(1) app_nil_end(2) Permutation_sym(3) ]
Permutation_trans(3) list_ind(2) Permutation_refl(2) app_comm_cons(1)
eq_ind_r(1) eq_ind(2) app_nil_end(2) Permutation_sym(3) ]

0 comments on commit 4904006

Please sign in to comment.