Skip to content

Commit bbd46c5

Browse files
proux01proux01
authored
Merge pull request #136 from coq-community/stdlib_repo
Adapt to rocq-prover/rocq#19530
2 parents 2a7a8f7 + 0ed4146 commit bbd46c5

File tree

5 files changed

+107
-107
lines changed

5 files changed

+107
-107
lines changed

‎tests/Morph_rw.dot.oracle

+10-10
Original file line numberDiff line numberDiff line change
@@ -6,27 +6,27 @@ Morphisms_trans_sym_co_inv_impl_morphism [label="trans_sym_co_inv_impl_morphism"
66
Morph_FsmpM_Proper [label="FsmpM_Proper", URL=<Morph.html#FsmpM_Proper>, fillcolor="#FFB57F"] ;
77
Morph_F [label="F", URL=<Morph.html#F>, fillcolor="#FACDEF"] ;
88
Morph_Fsmp [label="Fsmp", URL=<Morph.html#Fsmp>, fillcolor="#FACDEF"] ;
9-
RelationClasses_Equivalence_PER [label="Equivalence_PER", URL=<RelationClasses.html#Equivalence_PER>, fillcolor="#7FFFD4"] ;
109
Morph_Fequiv [label="Fequiv", URL=<Morph.html#Fequiv>, fillcolor="#FACDEF"] ;
10+
RelationClasses_Equivalence_PER [label="Equivalence_PER", URL=<RelationClasses.html#Equivalence_PER>, fillcolor="#7FFFD4"] ;
1111
Morph_FequivR [label="FequivR", URL=<Morph.html#FequivR>, fillcolor="#7FFFD4"] ;
1212
Morph_Fequiv_trans [label="Fequiv_trans", URL=<Morph.html#Fequiv_trans>, fillcolor="#FFB57F"] ;
1313
Morph_Fequiv_refl [label="Fequiv_refl", URL=<Morph.html#Fequiv_refl>, fillcolor="#FFB57F"] ;
1414
Morph_Fequiv_sym [label="Fequiv_sym", URL=<Morph.html#Fequiv_sym>, fillcolor="#FFB57F"] ;
1515
RelationClasses_Equivalence [label="Equivalence", URL=<RelationClasses.html#Equivalence>, fillcolor="#E2CDFA"] ;
1616
RelationClasses_Build_Equivalence [label="Build_Equivalence", URL=<RelationClasses.html#Build_Equivalence>, fillcolor="#7FAAFF"] ;
17+
RelationClasses_Symmetric [label="Symmetric", URL=<RelationClasses.html#Symmetric>, fillcolor="#F070D1"] ;
1718
RelationClasses_Reflexive [label="Reflexive", URL=<RelationClasses.html#Reflexive>, fillcolor="#F070D1"] ;
1819
Relation_Definitions_relation [label="relation", URL=<Relation_Definitions.html#relation>, fillcolor="#F070D1"] ;
1920
RelationClasses_Transitive [label="Transitive", URL=<RelationClasses.html#Transitive>, fillcolor="#F070D1"] ;
20-
RelationClasses_Symmetric [label="Symmetric", URL=<RelationClasses.html#Symmetric>, fillcolor="#F070D1"] ;
2121
RelationClasses_Equivalence_Transitive [label="Equivalence_Transitive", URL=<RelationClasses.html#Equivalence_Transitive>, fillcolor="#7FFFD4"] ;
2222
RelationClasses_Equivalence_Symmetric [label="Equivalence_Symmetric", URL=<RelationClasses.html#Equivalence_Symmetric>, fillcolor="#7FFFD4"] ;
2323
RelationClasses_PER [label="PER", URL=<RelationClasses.html#PER>, fillcolor="#E2CDFA"] ;
2424
RelationClasses_Build_PER [label="Build_PER", URL=<RelationClasses.html#Build_PER>, fillcolor="#7FAAFF"] ;
2525
Morphisms_Proper [label="Proper", URL=<Morphisms.html#Proper>, fillcolor="#F070D1"] ;
2626
Morphisms_respectful [label="respectful", URL=<Morphisms.html#respectful>, fillcolor="#F070D1"] ;
27-
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"] ;
2827
Basics_flip [label="flip", URL=<Basics.html#flip>, fillcolor="#F070D1"] ;
2928
Basics_impl [label="impl", URL=<Basics.html#impl>, fillcolor="#F070D1"] ;
29+
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"] ;
3030
RelationClasses_PER_Symmetric [label="PER_Symmetric", URL=<RelationClasses.html#PER_Symmetric>, fillcolor="#7FFFD4"] ;
3131
RelationClasses_symmetry [label="symmetry", URL=<RelationClasses.html#symmetry>, fillcolor="#7FFFD4"] ;
3232
RelationClasses_PER_Transitive [label="PER_Transitive", URL=<RelationClasses.html#PER_Transitive>, fillcolor="#7FFFD4"] ;
@@ -42,11 +42,11 @@ RelationClasses_transitivity [label="transitivity", URL=<RelationClasses.html#tr
4242
Morph_FsmpM_Proper -> Morphisms_Proper [] ;
4343
Morph_FsmpM_Proper -> Morphisms_respectful [] ;
4444
Morph_Fsmp -> Morph_F [] ;
45+
Morph_Fequiv -> Morph_F [] ;
4546
RelationClasses_Equivalence_PER -> RelationClasses_Equivalence_Transitive [] ;
4647
RelationClasses_Equivalence_PER -> RelationClasses_Equivalence_Symmetric [] ;
4748
RelationClasses_Equivalence_PER -> RelationClasses_PER [] ;
4849
RelationClasses_Equivalence_PER -> RelationClasses_Build_PER [] ;
49-
Morph_Fequiv -> Morph_F [] ;
5050
Morph_FequivR -> Morph_Fequiv_trans [] ;
5151
Morph_FequivR -> Morph_Fequiv_refl [] ;
5252
Morph_FequivR -> Morph_Fequiv_sym [] ;
@@ -55,21 +55,21 @@ RelationClasses_transitivity [label="transitivity", URL=<RelationClasses.html#tr
5555
Morph_Fequiv_trans -> Morph_Fequiv [] ;
5656
Morph_Fequiv_refl -> Morph_Fequiv [] ;
5757
Morph_Fequiv_sym -> Morph_Fequiv [] ;
58+
RelationClasses_Equivalence -> RelationClasses_Symmetric [] ;
5859
RelationClasses_Equivalence -> RelationClasses_Reflexive [] ;
5960
RelationClasses_Equivalence -> RelationClasses_Transitive [] ;
60-
RelationClasses_Equivalence -> RelationClasses_Symmetric [] ;
61+
RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ;
6162
RelationClasses_Build_Equivalence -> RelationClasses_Reflexive [] ;
6263
RelationClasses_Build_Equivalence -> RelationClasses_Transitive [] ;
63-
RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ;
64+
RelationClasses_Symmetric -> Relation_Definitions_relation [] ;
6465
RelationClasses_Reflexive -> Relation_Definitions_relation [] ;
6566
RelationClasses_Transitive -> Relation_Definitions_relation [] ;
66-
RelationClasses_Symmetric -> Relation_Definitions_relation [] ;
6767
RelationClasses_Equivalence_Transitive -> RelationClasses_Equivalence [] ;
6868
RelationClasses_Equivalence_Symmetric -> RelationClasses_Equivalence [] ;
69-
RelationClasses_PER -> RelationClasses_Transitive [] ;
7069
RelationClasses_PER -> RelationClasses_Symmetric [] ;
71-
RelationClasses_Build_PER -> RelationClasses_Transitive [] ;
70+
RelationClasses_PER -> RelationClasses_Transitive [] ;
7271
RelationClasses_Build_PER -> RelationClasses_Symmetric [] ;
72+
RelationClasses_Build_PER -> RelationClasses_Transitive [] ;
7373
Morphisms_Proper -> Relation_Definitions_relation [] ;
7474
Morphisms_respectful -> Relation_Definitions_relation [] ;
7575
Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Morphisms_respectful [] ;
@@ -86,7 +86,7 @@ RelationClasses_transitivity [label="transitivity", URL=<RelationClasses.html#tr
8686
subgraph cluster_Basics { label="Basics"; fillcolor="#FFFFC3"; labeljust=l; style=filled
8787
Basics_impl; Basics_flip; };
8888
subgraph cluster_RelationClasses { label="RelationClasses"; fillcolor="#FFFFC3"; labeljust=l; style=filled
89-
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; };
89+
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; };
9090
subgraph cluster_Morphisms { label="Morphisms"; fillcolor="#FFFFC3"; labeljust=l; style=filled
9191
Morphisms_trans_sym_co_inv_impl_morphism_obligation_1; Morphisms_respectful; Morphisms_Proper; Morphisms_trans_sym_co_inv_impl_morphism; };
9292
subgraph cluster_Relation_Definitions { label="Relation_Definitions"; fillcolor="#FFFFC3"; labeljust=l; style=filled

‎tests/Morph_rw.dpd.oracle

+49-49
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
N: 20 "Equivalence_PER" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
1+
N: 21 "Equivalence_PER" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
22
N: 33 "Equivalence_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
33
N: 32 "Equivalence_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
44
N: 18 "F" [body=no, kind=cnst, prop=no, path="Morph", ];
5-
N: 21 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ];
5+
N: 20 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ];
66
N: 22 "FequivR" [body=yes, kind=cnst, prop=yes, path="Morph", ];
77
N: 24 "Fequiv_refl" [body=no, kind=cnst, prop=yes, path="Morph", ];
88
N: 25 "Fequiv_sym" [body=no, kind=cnst, prop=yes, path="Morph", ];
@@ -12,17 +12,17 @@ N: 17 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ];
1212
N: 41 "PER_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
1313
N: 43 "PER_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
1414
N: 36 "Proper" [body=yes, kind=cnst, prop=no, path="Morphisms", ];
15-
N: 28 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
16-
N: 31 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
17-
N: 30 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
18-
N: 39 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ];
19-
N: 40 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ];
20-
N: 29 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ];
15+
N: 29 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
16+
N: 28 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
17+
N: 31 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ];
18+
N: 38 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ];
19+
N: 39 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ];
20+
N: 30 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ];
2121
N: 37 "respectful" [body=yes, kind=cnst, prop=no, path="Morphisms", ];
2222
N: 15 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ];
2323
N: 42 "symmetry" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
2424
N: 16 "trans_sym_co_inv_impl_morphism" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
25-
N: 38 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
25+
N: 40 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ];
2626
N: 44 "transitivity" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ];
2727
N: 26 "Equivalence" [kind=inductive, prop=no, path="RelationClasses", ];
2828
N: 34 "PER" [kind=inductive, prop=no, path="RelationClasses", ];
@@ -32,10 +32,10 @@ E: 15 16 [weight=1, ];
3232
E: 15 17 [weight=1, ];
3333
E: 15 18 [weight=6, ];
3434
E: 15 19 [weight=5, ];
35-
E: 15 20 [weight=1, ];
36-
E: 15 21 [weight=8, ];
35+
E: 15 20 [weight=8, ];
36+
E: 15 21 [weight=1, ];
3737
E: 15 22 [weight=1, ];
38-
E: 16 29 [weight=3, ];
38+
E: 16 30 [weight=3, ];
3939
E: 16 34 [weight=3, ];
4040
E: 16 36 [weight=1, ];
4141
E: 16 37 [weight=1, ];
@@ -44,30 +44,30 @@ E: 16 39 [weight=1, ];
4444
E: 16 40 [weight=1, ];
4545
E: 17 18 [weight=4, ];
4646
E: 17 19 [weight=1, ];
47-
E: 17 21 [weight=2, ];
47+
E: 17 20 [weight=2, ];
4848
E: 17 36 [weight=1, ];
4949
E: 17 37 [weight=1, ];
5050
E: 19 18 [weight=2, ];
51-
E: 20 26 [weight=2, ];
52-
E: 20 29 [weight=2, ];
53-
E: 20 32 [weight=1, ];
54-
E: 20 33 [weight=1, ];
55-
E: 20 34 [weight=1, ];
56-
E: 20 35 [weight=1, ];
57-
E: 21 18 [weight=2, ];
51+
E: 20 18 [weight=2, ];
52+
E: 21 26 [weight=2, ];
53+
E: 21 30 [weight=2, ];
54+
E: 21 32 [weight=1, ];
55+
E: 21 33 [weight=1, ];
56+
E: 21 34 [weight=1, ];
57+
E: 21 35 [weight=1, ];
5858
E: 22 18 [weight=2, ];
59-
E: 22 21 [weight=2, ];
59+
E: 22 20 [weight=2, ];
6060
E: 22 23 [weight=1, ];
6161
E: 22 24 [weight=1, ];
6262
E: 22 25 [weight=1, ];
6363
E: 22 26 [weight=1, ];
6464
E: 22 27 [weight=1, ];
6565
E: 23 18 [weight=3, ];
66-
E: 23 21 [weight=3, ];
66+
E: 23 20 [weight=3, ];
6767
E: 24 18 [weight=1, ];
68-
E: 24 21 [weight=1, ];
68+
E: 24 20 [weight=1, ];
6969
E: 25 18 [weight=2, ];
70-
E: 25 21 [weight=2, ];
70+
E: 25 20 [weight=2, ];
7171
E: 26 28 [weight=1, ];
7272
E: 26 29 [weight=1, ];
7373
E: 26 30 [weight=1, ];
@@ -76,39 +76,39 @@ E: 27 28 [weight=1, ];
7676
E: 27 29 [weight=1, ];
7777
E: 27 30 [weight=1, ];
7878
E: 27 31 [weight=1, ];
79-
E: 28 29 [weight=2, ];
80-
E: 30 29 [weight=2, ];
81-
E: 31 29 [weight=2, ];
79+
E: 28 30 [weight=2, ];
80+
E: 29 30 [weight=2, ];
81+
E: 31 30 [weight=2, ];
8282
E: 32 26 [weight=3, ];
83-
E: 32 29 [weight=2, ];
8483
E: 32 30 [weight=2, ];
84+
E: 32 31 [weight=2, ];
8585
E: 33 26 [weight=3, ];
86-
E: 33 29 [weight=2, ];
87-
E: 33 31 [weight=2, ];
88-
E: 34 29 [weight=1, ];
86+
E: 33 28 [weight=2, ];
87+
E: 33 30 [weight=2, ];
88+
E: 34 28 [weight=1, ];
8989
E: 34 30 [weight=1, ];
9090
E: 34 31 [weight=1, ];
91-
E: 35 29 [weight=1, ];
91+
E: 35 28 [weight=1, ];
9292
E: 35 30 [weight=1, ];
9393
E: 35 31 [weight=1, ];
94-
E: 36 29 [weight=2, ];
95-
E: 37 29 [weight=5, ];
96-
E: 38 29 [weight=2, ];
97-
E: 38 34 [weight=2, ];
98-
E: 38 37 [weight=1, ];
99-
E: 38 39 [weight=1, ];
100-
E: 38 40 [weight=1, ];
101-
E: 38 41 [weight=1, ];
102-
E: 38 42 [weight=1, ];
103-
E: 38 43 [weight=1, ];
104-
E: 38 44 [weight=1, ];
105-
E: 41 29 [weight=2, ];
106-
E: 41 31 [weight=2, ];
94+
E: 36 30 [weight=2, ];
95+
E: 37 30 [weight=5, ];
96+
E: 40 30 [weight=2, ];
97+
E: 40 34 [weight=2, ];
98+
E: 40 37 [weight=1, ];
99+
E: 40 38 [weight=1, ];
100+
E: 40 39 [weight=1, ];
101+
E: 40 41 [weight=1, ];
102+
E: 40 42 [weight=1, ];
103+
E: 40 43 [weight=1, ];
104+
E: 40 44 [weight=1, ];
105+
E: 41 28 [weight=2, ];
106+
E: 41 30 [weight=2, ];
107107
E: 41 34 [weight=3, ];
108-
E: 42 29 [weight=2, ];
109-
E: 42 31 [weight=2, ];
110-
E: 43 29 [weight=2, ];
108+
E: 42 28 [weight=2, ];
109+
E: 42 30 [weight=2, ];
111110
E: 43 30 [weight=2, ];
111+
E: 43 31 [weight=2, ];
112112
E: 43 34 [weight=3, ];
113-
E: 44 29 [weight=2, ];
114113
E: 44 30 [weight=2, ];
114+
E: 44 31 [weight=2, ];

‎tests/graph2.dot.oracle

+11-11
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ digraph tests/graph2 {
44
Test_Permutation_app_swap [label="Permutation_app_swap", URL=<Test.html#Permutation_app_swap>, peripheries=3, fillcolor="#7FFFD4"] ;
55
Test_Permutation_sym [label="Permutation_sym", URL=<Test.html#Permutation_sym>, fillcolor="#7FFFD4"] ;
66
Test_app_nil_end [label="app_nil_end", URL=<Test.html#app_nil_end>, fillcolor="#7FFFD4"] ;
7-
_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ;
8-
_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ;
97
Test_app_comm_cons [label="app_comm_cons", URL=<Test.html#app_comm_cons>, fillcolor="#7FFFD4"] ;
108
Test_Permutation_refl [label="Permutation_refl", URL=<Test.html#Permutation_refl>, fillcolor="#7FFFD4"] ;
119
Test_list_ind [label="list_ind", URL=<Test.html#list_ind>, fillcolor="#7FFFD4"] ;
10+
_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ;
11+
_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ;
1212
Test_Permutation_trans [label="Permutation_trans", URL=<Test.html#Permutation_trans>, fillcolor="#7FFFD4"] ;
1313
Test_app [label="app", URL=<Test.html#app>, fillcolor="#F070D1"] ;
1414
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
1818
Test_nil [label="nil", URL=<Test.html#nil>, fillcolor="#7FAAFF"] ;
1919
Test_cons [label="cons", URL=<Test.html#cons>, fillcolor="#7FAAFF"] ;
2020
Test_perm_trans [label="perm_trans", URL=<Test.html#perm_trans>, fillcolor="#7FAAFF"] ;
21-
Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
21+
_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
2222
_eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ;
2323
_eq_refl [label="eq_refl", URL=<.html#eq_refl>, fillcolor="#7FAAFF"] ;
24-
_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ;
24+
Test_perm_nil [label="perm_nil", URL=<Test.html#perm_nil>, fillcolor="#7FAAFF"] ;
2525
Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>, fillcolor="#7FFFD4"] ;
2626
Test_Permutation_app_swap -> Test_Permutation_sym [] ;
2727
Test_Permutation_app_swap -> Test_app_nil_end [] ;
28-
Test_Permutation_app_swap -> _eq_ind_r [] ;
2928
Test_Permutation_app_swap -> Test_app_comm_cons [] ;
3029
Test_Permutation_app_swap -> Test_Permutation_refl [] ;
30+
Test_Permutation_app_swap -> _eq_ind_r [] ;
3131
Test_Permutation_app_swap -> Test_Permutation_trans [] ;
3232
Test_Permutation_sym -> Test_perm_skip [] ;
3333
Test_Permutation_sym -> Test_perm_swap [] ;
3434
Test_Permutation_sym -> Test_perm_trans [] ;
3535
Test_Permutation_sym -> Test_perm_nil [] ;
3636
Test_Permutation_sym -> Test_Permutation_ind [] ;
37-
Test_app_nil_end -> _eq_ind [] ;
3837
Test_app_nil_end -> Test_list_ind [] ;
38+
Test_app_nil_end -> _eq_ind [] ;
3939
Test_app_nil_end -> Test_app [] ;
4040
Test_app_nil_end -> _eq_refl [] ;
41-
_eq_ind -> _eq [] ;
42-
_eq_ind_r -> _eq_ind [] ;
43-
_eq_ind_r -> _eq_sym [] ;
4441
Test_app_comm_cons -> Test_app [] ;
4542
Test_app_comm_cons -> _eq [] ;
4643
Test_app_comm_cons -> _eq_refl [] ;
@@ -51,6 +48,9 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
5148
Test_list_ind -> Test_list [] ;
5249
Test_list_ind -> Test_nil [] ;
5350
Test_list_ind -> Test_cons [] ;
51+
_eq_ind -> _eq [] ;
52+
_eq_ind_r -> _eq_ind [] ;
53+
_eq_ind_r -> _eq_sym [] ;
5454
Test_Permutation_trans -> Test_Permutation [] ;
5555
Test_Permutation_trans -> Test_perm_trans [] ;
5656
Test_app -> Test_list [] ;
@@ -67,11 +67,11 @@ Test_Permutation_ind [label="Permutation_ind", URL=<Test.html#Permutation_ind>,
6767
Test_perm_trans -> Test_list [] ;
6868
Test_perm_trans -> Test_nil [] ;
6969
Test_perm_trans -> Test_cons [] ;
70+
_eq_sym -> _eq [] ;
71+
_eq_sym -> _eq_refl [] ;
7072
Test_perm_nil -> Test_list [] ;
7173
Test_perm_nil -> Test_nil [] ;
7274
Test_perm_nil -> Test_cons [] ;
73-
_eq_sym -> _eq [] ;
74-
_eq_sym -> _eq_refl [] ;
7575
Test_Permutation_ind -> Test_Permutation [] ;
7676
subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled
7777
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; };

0 commit comments

Comments
 (0)