summaryrefslogtreecommitdiff
path: root/common/Globalenvs.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-03-11 16:13:15 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-03-11 16:13:15 +0000
commite2fb435c257cf6aac24e7b30f902bede694100c5 (patch)
tree7c498eb9dbed3d4c194fc965704e5ed57e75672f /common/Globalenvs.v
parentc7a642bf2156221a5c93826444e5e49ebb3b682b (diff)
Minor updates
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1848 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Globalenvs.v')
-rw-r--r--common/Globalenvs.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 367f44a..e01d5f7 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -3,7 +3,7 @@
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* with contributions from Andrew Tolmach (Portland State University) *)
+(* with contributions from Andrew Tolmach (Portland State University) *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
@@ -1477,7 +1477,7 @@ Proof.
apply find_funct_ptr_match. auto.
Qed.
-Theorem find_funct_rev_match: (* a little weak *)
+Theorem find_funct_rev_match:
forall (v : val) (tf : B),
find_funct (globalenv p') v = Some tf ->
(exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf)