All exported names are now qualified. This avoids the need for "open" statements.

diff --git a/helm/software/components/cic_exportation/cicExportation.mli b/helm/software/components/cic_exportation/cicExportation.mli
index 07c2b88455a0e3c069552ec48bda1e4919906bb6..1f68e4e75e57e8e62e9e8f11f24db67050e0ac16 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.mli
+++ b/helm/software/components/cic_exportation/cicExportation.mli
@@ -25,4 +25,5 @@
 
 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
 
-val ppobj : Cic.obj -> string
+(* ppobj current_module_name obj *)
+val ppobj : string -> Cic.obj -> string

diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend
index bb3e16d8e8bc73402a1f0b0263114ed06b97aea3..964011bfd1609a0355170ca53b1024c22970af70 100644 (file)
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -31,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
 declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi