diff options
| author | Pierre-Marie Pédrot | 2020-11-14 20:47:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:28:27 +0100 |
| commit | 3c9908f9b7c73af2ad9c617b3ced424dca2fcb2e (patch) | |
| tree | 909bcaab3c13177663692da40b7e3ac59d1cf32e | |
| parent | 68cd077344ce37db1a601079dbc4fdcae6c8d41f (diff) | |
Fix test-suite.
| -rw-r--r-- | test-suite/output/TypeclassDebug.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v index 2e4008ae56..0bd3d5fa40 100644 --- a/test-suite/output/TypeclassDebug.v +++ b/test-suite/output/TypeclassDebug.v @@ -2,6 +2,7 @@ Parameter foo : Prop. Axiom H : foo -> foo. +#[global] Hint Resolve H : foo. Goal foo. Typeclasses eauto := debug. |