Commit fc36dc52 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

missing dot pattern, rule was never triggered

parent 962d9ff9
......@@ -220,7 +220,7 @@ Ot_eq_po : A : ObjType ->
H : (l : Label ->
Istrue (domain_mem l dk_domain.nil) ->
Istrue (Ot_eq (Ot_assoc B2 l) (Ot_assoc B1 l))) ]
Ot_eq_po A B1 B2 dk_domain.nil H (Po_nil A (Ot_assoc B1))
Ot_eq_po A B1 B2 dk_domain.nil H (Po_nil A { Ot_assoc B1 })
-->
Po_nil A (Ot_assoc B2)
[ A : ObjType,
......@@ -232,8 +232,8 @@ Ot_eq_po : A : ObjType ->
H : l2 : Label ->
Istrue (domain_mem l2 (dk_domain.cons l C)) ->
Istrue (Ot_eq (Ot_assoc B2 l2) (Ot_assoc B1 l2)),
o : PreObj A (Ot_assoc B1) C]
Ot_eq_po A B1 B2 (dk_domain.cons l C) H (Po_cons A (Ot_assoc B1) C l m o)
o : PreObj A (Ot_assoc B1) C ]
Ot_eq_po A B1 B2 (dk_domain.cons l C) H (Po_cons A { Ot_assoc B1 } C l m o)
-->
Po_cons
A
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment