aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
-rw-r--r--plugins/ltac/tacinterp.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fcdf7bb2c..b8c021f18 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
open Tacmach.New
open Tactic_debug
open Constrexpr
-open Term
open Termops
open Tacexpr
open Genarg