From b27ed35711b59b034dd3900dbca26ac190713cea Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 13 Mar 2020 11:44:58 +0100
Subject: fmap_sem

---
 backend/CSE3analysisproof.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 7a74e623..155fedef 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -216,9 +216,9 @@ Definition eq_involves (eq : equation) (i : reg) :=
   i = (eq_lhs eq) \/ In i (eq_args eq).
 
 Section SOUNDNESS.
-  Variable F V : Type.
-  Variable genv: Genv.t F V.
-  Variable sp : val.
+  Context {F V : Type}.
+  Context {genv: Genv.t F V}.
+  Context {sp : val}.
 
   Context {ctx : eq_context}.
 
-- 
cgit