From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 17:25:25 +0000 (+0000) Subject: All exported names are now qualified. This avoids the need for "open" statements. X-Git-Tag: 0.4.95@7852~64 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b617e876fb237d885e1160c7fb1c6f392017d7ec All exported names are now qualified. This avoids the need for "open" statements. --- diff --git a/components/cic_exportation/cicExportation.mli b/components/cic_exportation/cicExportation.mli index 07c2b8845..1f68e4e75 100644 --- a/components/cic_exportation/cicExportation.mli +++ b/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/components/tactics/.depend b/components/tactics/.depend index bb3e16d8e..964011bfd 100644 --- a/components/tactics/.depend +++ b/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