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/Cshmgenproof.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/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index e373d4e5..d8653544 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1974,7 +1974,7 @@ End CORRECTNESS. (** ** Commutation with linking *) -Instance TransfCshmgenLink : TransfLink match_prog. +Global Instance TransfCshmgenLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2). generalize H. |