diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-10-29 21:56:59 +0200 |
commit | ae2d228c04f4fca1e281b146764646cbdd7d6b1d (patch) | |
tree | 244f88aebc77a9ca2ef7e69731deb1dfee434ece /cfrontend/SimplLocalsproof.v | |
parent | e19d179d1f30d5893e5f30dbd33188350656831e (diff) | |
parent | d194e47a7d494944385ff61c194693f8a67787cb (diff) | |
download | compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.tar.gz compcert-kvx-ae2d228c04f4fca1e281b146764646cbdd7d6b1d.zip |
Merge remote-tracking branch 'origin/master' into towards_3.10
Diffstat (limited to 'cfrontend/SimplLocalsproof.v')
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e4b759c4..c133d8ea 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -2320,7 +2320,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSimplLocalsLink : TransfLink match_prog. +Global Instance TransfSimplLocalsLink : TransfLink match_prog. Proof. red; intros. eapply Ctypes.link_match_program; eauto. - intros. |