]> matita.cs.unibo.it Git - helm.git/commitdiff
All exported names are now qualified. This avoids the need for "open" statements.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 17:25:25 +0000 (17:25 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 17:25:25 +0000 (17:25 +0000)
helm/software/components/cic_exportation/cicExportation.mli
helm/software/components/tactics/.depend

index 07c2b88455a0e3c069552ec48bda1e4919906bb6..1f68e4e75e57e8e62e9e8f11f24db67050e0ac16 100644 (file)
@@ -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
index bb3e16d8e8bc73402a1f0b0263114ed06b97aea3..964011bfd1609a0355170ca53b1024c22970af70 100644 (file)
@@ -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