Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

attempt at making all tests go through #135

Closed
wants to merge 1 commit into from
Closed

attempt at making all tests go through #135

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions tests/Morph_rw.dot.oracle
View file
Open in desktop
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_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 [] ;
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_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
Expand Down
68 changes: 34 additions & 34 deletions tests/Morph_rw.dpd.oracle
View file
Open in desktop
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: 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", ];
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 29 [weight=3, ];
E: 16 30 [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 29 [weight=2, ];
E: 20 30 [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 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, ];
1 change: 1 addition & 0 deletions tests/PrimitiveProjections.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions tests/Test.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
22 changes: 11 additions & 11 deletions tests/graph2.dot.oracle
View file
Open in desktop
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,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 [] ;
Expand All @@ -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 [] ;
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
Open in desktop
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: 190 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 188 "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: 189 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ];
N: 187 "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: 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: 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: 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: 201 "perm_nil" [kind=construct, prop=yes, path="Test", ];
N: 204 "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=2, ];
E: 184 188 [weight=1, ];
E: 184 189 [weight=1, ];
E: 184 187 [weight=1, ];
E: 184 188 [weight=2, ];
E: 184 189 [weight=2, ];
E: 184 190 [weight=2, ];
E: 184 191 [weight=2, ];
E: 184 191 [weight=1, ];
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 201 [weight=1, ];
E: 185 204 [weight=1, ];
E: 185 205 [weight=1, ];
E: 186 187 [weight=1, ];
E: 186 191 [weight=1, ];
E: 186 189 [weight=1, ];
E: 186 190 [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 202 [weight=3, ];
E: 188 187 [weight=1, ];
E: 188 202 [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: 188 204 [weight=1, ];
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: 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: 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 195 [weight=6, ];
E: 201 198 [weight=2, ];
E: 201 199 [weight=6, ];
E: 204 202 [weight=5, ];
E: 204 203 [weight=1, ];
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: 205 194 [weight=10, ];
E: 205 195 [weight=22, ];
E: 205 198 [weight=4, ];
Expand Down
6 changes: 3 additions & 3 deletions tests/search.oracle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Welcome to Coq
[Loading ML file coq-dpdgraph.plugin ... done]
[Loading ML file coq-core.plugins.ring ... done]
[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) list_ind(2) Permutation_refl(2) app_comm_cons(1)
eq_ind_r(1) eq_ind(2) app_nil_end(2) Permutation_sym(3) ]
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) ]
Loading