From 94126f45582b7f02a6c16284cdc627b7b0fe53ac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 19:44:21 +0200 Subject: 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. --- test-suite/success/Scopes.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'test-suite/success') 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). + -- cgit v1.2.3