diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:33:57 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:33:57 +0100 |
| commit | e2d7bba73f52285475da813433c703d7df7ae44a (patch) | |
| tree | 370ace815a967f1847103e4a26f7b94c81dc323d /src/hls/HashTree.v | |
| parent | 405e822a4e769969ef01a683d486accee0d71da2 (diff) | |
| download | vericert-e2d7bba73f52285475da813433c703d7df7ae44a.tar.gz vericert-e2d7bba73f52285475da813433c703d7df7ae44a.zip | |
Update to Coq 8.17 and CompCert 3.12
Diffstat (limited to 'src/hls/HashTree.v')
| -rw-r--r-- | src/hls/HashTree.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index 7387401..a088a54 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -498,14 +498,14 @@ Module HashTree(H: Hashable). forall x, match_one x x. Proof. unfold match_one; auto. Qed. - Instance match_one_Reflexive : Reflexive match_one. + #[global] Instance match_one_Reflexive : Reflexive match_one. Proof. unfold Reflexive. auto using match_one_refl. Qed. Lemma match_one_trans : forall x y z, match_one x y -> match_one y z -> match_one x z. Proof. unfold match_one; auto. Qed. - Instance match_one_Transitive : Transitive match_one. + #[global] Instance match_one_Transitive : Transitive match_one. Proof. unfold Transitive. eauto using match_one_trans. Qed. Lemma hash_value_gt : |