- 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 b8490f0592a91fa522cd3d44586d8e7e8120e35b..2c1b1883b930c5165aed955c41e864af88465f99 100644 (file)
--- a/helm/gTopLevel/tacticals.ml
+++ b/helm/gTopLevel/tacticals.ml
@@ -24,14 +24,13 @@
  *)
 
 open CicReduction
-open PrimitiveTactics
 open ProofEngineTypes
 open UriManager
 
 (** DEBUGGING *)
 
   (** perform debugging output? *)
-let debug = true
+let debug = false
 
   (** debugging print *)
 let warn s =