From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 27 Apr 2017 21:58:52 +0200 Subject: Post-rebase warnings (unused opens and 2 unused values) --- tactics/auto.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 324c551d0..c2d12ebd0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,15 +10,12 @@ module CVars = Vars open Pp open Util -open CErrors open Names open Termops open EConstr open Environ -open Tacmach open Genredexpr open Tactics -open Tacticals open Clenv open Locus open Proofview.Notations -- cgit v1.2.3