diff options
Diffstat (limited to 'test-suite/output/relaxed_ambiguous_paths.v')
| -rw-r--r-- | test-suite/output/relaxed_ambiguous_paths.v | 72 |
1 files changed, 49 insertions, 23 deletions
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v index 41322045f2..182e155273 100644 --- a/test-suite/output/relaxed_ambiguous_paths.v +++ b/test-suite/output/relaxed_ambiguous_paths.v @@ -1,13 +1,20 @@ Module test1. Section test1. -Variable (A B C D : Type). -Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D). - -Local Coercion ab : A >-> B. -Local Coercion bd : B >-> D. -Local Coercion ac : A >-> C. -Local Coercion cd : C >-> D. +Variable (A B C A' B' C' : Type). +Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C'). +Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C'). + +Local Coercion g1 : A >-> B. +Local Coercion g2 : A' >-> B'. +Local Coercion h1 : B >-> C. +Local Coercion h2 : B' >-> C'. +Local Coercion f1 : A >-> A'. +Local Coercion f2 : B >-> B'. +Local Coercion f3 : C >-> C'. +(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous *) +(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and *) +(* `[h1; f3], [f2; h2] : B >-> C'`. *) Print Graph. @@ -24,8 +31,8 @@ Local Coercion ac : A >-> C. Local Coercion cd : C >-> D. Local Coercion ab : A >-> B. Local Coercion bc : B >-> C. -(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *) -(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *) +(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous *) +(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`. *) Print Graph. @@ -34,6 +41,25 @@ End test2. Module test3. Section test3. + +Variable (A B C : Type). +Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C). + +Local Coercion ac : A >-> C. +Local Coercion bc : B >-> C. +Local Coercion ab : A >-> B. +Local Coercion ba : B >-> A. +(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths *) +(* because they are redundant with `[ab; bc], [ac] : A >-> C` and *) +(* `[ba; ab] : B >-> B`. *) + +Print Graph. + +End test3. +End test3. + +Module test4. +Section test4. Variable (A : Type) (P Q : A -> Prop). Record B := { @@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d). Print Graph. -End test3. -End test3. +End test4. +End test4. -Module test4. -Section test4. +Module test5. +Section test5. Variable (A : Type) (P Q : A -> Prop). @@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d). Print Graph. -End test4. -End test4. +End test5. +End test5. -Module test5. -Section test5. +Module test6. +Section test6. Variable (A : Type) (P Q : A -> Prop). @@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true := Print Graph. -End test5. -End test5. +End test6. +End test6. -Module test6. +Module test7. Record > NAT := wrap_nat { unwrap_nat :> nat }. Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE := wrap_Type { unwrap_Type :> Type }. -End test6. +End test7. -Module test7. +Module test8. Set Primitive Projections. Record > NAT_prim := wrap_nat { unwrap_nat :> nat }. Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }. -End test7. +End test8. |