From a90f984e511b2c6a7623465f5dfd7956b7263705 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Jun 2005 15:41:37 +0000 Subject: [PATCH] removed profiling function (now a stub is used instead) added a comment in urimanager --- helm/ocaml/cic/cicUtil.ml | 3 +++ helm/ocaml/tactics/.depend | 34 +++++++++++++--------------- helm/ocaml/urimanager/uriManager.mli | 2 +- 3 files changed, 20 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index d3fcffd80..8de1ce2a2 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -224,3 +224,6 @@ let profile = print_endline ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); profile + + (** WARNING: COMMENT THIS TO ENABLE PROFILING **) +let profile _ = let profile f x = f x in profile diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 9efaac2b9..481447099 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -33,9 +33,9 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi + proofEngineHelpers.cmi primitiveTactics.cmi primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi + proofEngineHelpers.cmx primitiveTactics.cmi hashtbl_equiv.cmo: hashtbl_equiv.cmi hashtbl_equiv.cmx: hashtbl_equiv.cmi metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ @@ -67,13 +67,11 @@ negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \ negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \ primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineStructuralRules.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ - equalityTactics.cmi + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + introductionTactics.cmi equalityTactics.cmi equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineStructuralRules.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ - equalityTactics.cmi + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + introductionTactics.cmx equalityTactics.cmi discriminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ eliminationTactics.cmi discriminationTactics.cmi @@ -102,13 +100,13 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi ring.cmi reductionTactics.cmi \ - primitiveTactics.cmi negationTactics.cmi introductionTactics.cmi \ - fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \ - eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi \ - tactics.cmi -tactics.cmx: variousTactics.cmx ring.cmx reductionTactics.cmx \ - primitiveTactics.cmx negationTactics.cmx introductionTactics.cmx \ - fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ - eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx \ - tactics.cmi +tactics.cmo: variousTactics.cmi tacticals.cmi ring.cmi reductionTactics.cmi \ + proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ + introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ + equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ + autoTactic.cmi tactics.cmi +tactics.cmx: variousTactics.cmx tacticals.cmx ring.cmx reductionTactics.cmx \ + proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ + introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ + equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ + autoTactic.cmx tactics.cmi diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index bed9db29e..86cd5c142 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -34,7 +34,7 @@ val uri_of_string : string -> uri val string_of_uri : uri -> string (* complete uri *) val name_of_uri : uri -> string (* name only (without extension)*) -val buri_of_uri : uri -> string (* base uri only *) +val buri_of_uri : uri -> string (* base uri only, without trailing '/' *) (* given an uri, returns the uri of the corresponding cic file, *) (* i.e. removes the [.types][.ann] suffix *) -- 2.39.2