diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-01 19:44:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 01:58:11 +0200 |
| commit | 94126f45582b7f02a6c16284cdc627b7b0fe53ac (patch) | |
| tree | 0cb5eff7c80ae45ccf091e620a3ba4257a7fa389 /test-suite/success | |
| parent | a3407e27e60104fa8ea2e62433f9920a41a22757 (diff) | |
Factorizing interp_gen through a function interpreting glob_constr.
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
Diffstat (limited to 'test-suite/success')
| -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 43e3493c1..ca3746716 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). + |