Ajout du Let pour le langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)