diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 11:44:58 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 11:44:58 +0100 |
| commit | b27ed35711b59b034dd3900dbca26ac190713cea (patch) | |
| tree | cd7a92fb65f20b03ebf80517008e2f48ac0d0c43 /backend/CSE3analysisproof.v | |
| parent | 085e4f45ebf81b7734efa70f018928ac49703f47 (diff) | |
| download | compcert-kvx-b27ed35711b59b034dd3900dbca26ac190713cea.tar.gz compcert-kvx-b27ed35711b59b034dd3900dbca26ac190713cea.zip | |
fmap_sem
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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}. |