aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/coq_omega.ml1
-rw-r--r--plugins/omega/g_omega.ml41
2 files changed, 0 insertions, 2 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 74f1ba713f..de20756b3c 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -27,7 +27,6 @@ open Globnames
open Nametab
open Contradiction
open Misctypes
-open Proofview.Notations
module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
open OmegaSolver
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 0aad364c16..b384478ae2 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -16,7 +16,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Coq_omega
-open Refiner
let omega_tactic l =
let tacs = List.map