aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml4')
-rw-r--r--tactics/class_tactics.ml414
1 files changed, 0 insertions, 14 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 933bb6619..d411a28c4 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -12,29 +12,16 @@ open Pp
open Errors
open Util
open Names
-open Nameops
open Term
open Termops
-open Sign
open Reduction
open Proof_type
-open Declarations
open Tacticals
open Tacmach
-open Evar_refiner
open Tactics
-open Pattern
open Patternops
open Clenv
-open Auto
-open Glob_term
-open Hiddentac
open Typeclasses
-open Typeclasses_errors
-open Classes
-open Topconstr
-open Pfedit
-open Command
open Globnames
open Evd
open Locus
@@ -750,7 +737,6 @@ VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
END
open Genarg
-open Extraargs
let pr_debug _prc _prlc _prt b =
if b then Pp.str "debug" else Pp.mt()