diff options
Diffstat (limited to 'theories/FSets/FSetDecide.v')
| -rw-r--r-- | theories/FSets/FSetDecide.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 8a217a752a..d597c0404a 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -466,6 +466,7 @@ the above form: (** Here is the tactic that will throw away hypotheses that are not useful (for the intended scope of the [fsetdec] tactic). *) + #[global] Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop. Ltac discard_nonFSet := repeat ( @@ -518,6 +519,7 @@ the above form: (** The hint database [FSet_decidability] will be given to the [push_neg] tactic from the module [Negation]. *) + #[global] Hint Resolve dec_In dec_eq : FSet_decidability. (** ** Normalizing Propositions About Equality |