From af4311b5fe3b3836f9464c8d8f6ca737307a6a2f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 May 2006 12:07:36 +0000 Subject: [PATCH] added important comment --- helm/software/components/tactics/paramodulation/equality.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 57c440860..5f847bcb5 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -502,6 +502,9 @@ let pp_proof names goalproof proof = let get_duplicate_step_in_wfo l p = let ol = List.rev l in let h = Hashtbl.create 13 in + (* NOTE: here the n parameter is an approximation of the dependency + between equations. To do things seriously we should maintain a + dependency graph. This approximation is not perfect. *) let add i n = let p,_,_ = proof_of_id i in match p with -- 2.39.2