diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 17:10:01 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 17:10:01 +0100 |
| commit | 3f33a6e366b0c018690c2b3246eb303c5eb57f46 (patch) | |
| tree | c2f4509e526bdd83da42ca8d8c8af4076fdf3312 /lib | |
| parent | 3c34c386912e904b432c53e1dbb2b3dda3f8501f (diff) | |
| download | compcert-kvx-3f33a6e366b0c018690c2b3246eb303c5eb57f46.tar.gz compcert-kvx-3f33a6e366b0c018690c2b3246eb303c5eb57f46.zip | |
kill_reg_sound
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/HashedSet.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/HashedSet.v b/lib/HashedSet.v index 5b4faeaa..bd9cd9c0 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -52,7 +52,7 @@ Proof. destruct b; reflexivity. Qed. -Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false: pset. +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pset. Module PSet_internals. Inductive pset : Type := |