diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:14:27 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-11 13:14:52 +0200 |
| commit | e0577588056110ea13a904aa1f01c86dbc931f02 (patch) | |
| tree | 5a266c3a63a288976bc11f45c670de91e5595ae1 /tactics | |
| parent | e302b4dbc88c5776155c770aa90134edb571b738 (diff) | |
Remove an unused open introduced by the previous commit.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3842b432d..556df6e55 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5004,7 +5004,6 @@ let name_op_to_name name_op object_kind suffix = add_suffix name suffix, gk let tclABSTRACT ?(opaque=true) name_op tac = - let open Proof_global in let s, gk = if opaque then name_op_to_name name_op (Proof Theorem) "_subproof" else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in |