diff options
| author | Maxime Dénès | 2017-06-06 08:56:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 08:56:35 +0200 |
| commit | 98dc4f985f2ddd47b4d4d6afee901a0a2bb0bde0 (patch) | |
| tree | 9b8958585f6e593874f2deb789b2f01fb237637c /test-suite | |
| parent | 6e4d1ee9bb61601df041fe44eb60b4fa059080d5 (diff) | |
| parent | a07c0579a2d4b660b3b9996cd79bdf8e0f588949 (diff) | |
Merge PR#600: Some factorizations of ltac interpretation functions between ssreflect and coq code
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Scopes.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 43e3493c1e..ca37467166 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -20,3 +20,9 @@ Inductive U := A. Bind Scope u with U. Notation "'ε'" := A : u. Definition c := ε : U. + +(* Check activation of type scope for tactics such as assert *) + +Goal True. +assert (nat * nat). + |