aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/class.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml12
1 files changed, 9 insertions, 3 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 56077f36e..b6824dac7 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -19,9 +19,15 @@ open Declare
(* strength * strength -> bool *)
let stre_gt = function
- | (NeverDischarge,NeverDischarge) -> false
- | (NeverDischarge,x) -> false
- | (x,NeverDischarge) -> true
+(* | (x,y) when (x = NeverDischarge || x = NotDeclare)
+ && (y = NeverDischarge || y = NotDeclare) -> false
+ | (x,_) when x = NeverDischarge || x = NotDeclare -> false
+ | (_,x) when x = NeverDischarge || x = NotDeclare -> true*)
+
+ | (NeverDischarge,_) -> false
+ | (NotDeclare,_) -> false
+ | (_,NeverDischarge) -> true
+ | (_,NotDeclare) -> true
| (DischargeAt sp1,DischargeAt sp2) ->
dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *)