aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Compiler.vexpand2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index 9673267d..7503d3ed 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -163,7 +163,7 @@ Proof.
intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
Qed.
-Instance TransfIfLink {A: Type} {LA: Linker A}
+Global Instance TransfIfLink {A: Type} {LA: Linker A}
(flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf)
: TransfLink (match_if flag transf).
Proof.