aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4b03c935f..dd7542fc7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -16,7 +16,6 @@ open Libnames
open Globnames
open Termops
open Namegen
-open Libobject
open Environ
open Closure
open Reductionops