From b617e876fb237d885e1160c7fb1c6f392017d7ec Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 17:25:25 +0000 Subject: [PATCH] All exported names are now qualified. This avoids the need for "open" statements. --- components/cic_exportation/cicExportation.mli | 3 ++- components/tactics/.depend | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.2