aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/evar_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/evar_tactics.ml')
-rw-r--r--tactics/evar_tactics.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 20f72b3d5..83a98745a 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Util
-open Names
open Errors
open Evar_refiner
open Tacmach
@@ -50,7 +49,6 @@ let instantiate n (ist,rawc) ido gl =
tclNORMEVAR
gl
-open Proofview.Notations
let let_evar name typ =
let src = (Loc.ghost,Evar_kinds.GoalEvar) in
Proofview.Goal.enter begin fun gl ->