aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-06-17 14:26:02 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-06-17 15:44:38 +0200
commit90d64647d3fd5dbf5c337944dc0038f0b19b8a51 (patch)
treeb33528c72730ec541a75e3d0baaead6789f4dcb9 /plugins/firstorder/instances.ml
parentd412844753ef25f4431c209f47b97b9fa498297d (diff)
Removing dead code.
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 11b120c41..076107450 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Reductionops
open Formula
open Sequent
open Names
-open Globnames
open Misctypes
let compare_instance inst1 inst2=