Skip to content
Snippets Groups Projects
Commit 419e46bd authored by Ralf Jung's avatar Ralf Jung
Browse files

remove unnecessary 'Open Scope'

parent 797c02bd
No related branches found
No related tags found
No related merge requests found
......@@ -77,8 +77,6 @@ Module StringToIdent.
intros $ident).
End StringToIdent.
Global Open Scope string_scope.
(** Finally we wrap everything up intro a tactic that renames a variable given
by ident [id] into the name given by string [s].
Only works if [id] can be reverted, i.e. if nothing else depends on it. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment