From 3f33a6e366b0c018690c2b3246eb303c5eb57f46 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Mar 2020 17:10:01 +0100 Subject: kill_reg_sound --- lib/HashedSet.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/HashedSet.v') 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 := -- cgit