- ElimIntrosSimpl now implemented using tacticals. It becomes an

[helm.git] / helm / gTopLevel / tacticals.ml

diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml
index f3cd13b44c8f9544d766d027ef837242a977fbc9..2c1b1883b930c5165aed955c41e864af88465f99 100644 (file)
--- a/helm/gTopLevel/tacticals.ml
+++ b/helm/gTopLevel/tacticals.ml
@@ -24,7 +24,6 @@
  *)
 
 open CicReduction
-open PrimitiveTactics
 open ProofEngineTypes
 open UriManager