aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Coloringproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Coloringproof.v')
-rw-r--r--backend/Coloringproof.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index f3801d07..ce24030d 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -325,6 +325,7 @@ Proof.
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
apply add_interf_call_incl.
+ apply add_prefs_call_incl.
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_interf_op_incl].