From: Enrico Tassi Date: Wed, 26 Apr 2006 10:05:28 +0000 (+0000) Subject: more cleanup X-Git-Tag: make_still_working~7395 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1ff463fe4ae5c3f9ba10da0339aadc99169aef5;p=helm.git more cleanup --- diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 5cc6e811e..fac0197df 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -111,7 +111,8 @@ module OrderedEquality = struct match Pervasives.compare w1 w2 with | 0 -> let res = (List.length m1) - (List.length m2) in - if res <> 0 then res else Pervasives.compare eq1 eq2 + if res <> 0 then res else + Pervasives.compare eq1 eq2 | res -> res end @@ -1396,47 +1397,6 @@ let reset_refs () = Equality.reset (); ;; -let interactive_comparison context t1 t2 = - let rc = ref [] in - let module P = Printf in - let rec aux n context t1 t2 = -(* let names = names_of_context context in*) - let pp t1 t2 = () (* - P.eprintf "%s%s === %s\n" (String.make n ' ') - (CicPp.pp t1 names) (CicPp.pp t2 names) *) - in - match t1,t2 with - | _, Cic.Appl [Cic.Const(uri,_);t2] when - UriManager.eq uri (UriManager.uri_of_string - "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2 - | Cic.Implicit _, _ -> pp t1 t2 - | Cic.Meta (n,_), _ -> - rc := (n,t2,context) :: !rc; - pp (Cic.Meta(n,[])) t2 - | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2 - | Cic.Appl l1,Cic.Appl l2 -> - if List.length l1 <> List.length l2 then - begin - prerr_endline "ERROR: application with diff num of args"; - pp t1 t2 - end - else - List.iter2 (aux (n+1) context) l1 l2 - | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) -> - let context = (Some (name,(Cic.Decl s)))::context in - aux (n+1) context t1 t2 - | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 -> - pp t1 t2 - | _,_ -> pp t1 t2 - in - aux 0 context t1 t2; - List.iter (fun (n,t,ctx) -> - let names = names_of_context ctx in - Printf.eprintf "%d := %s\n" n (CicPp.pp t names)) - (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc)) -;; - - let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1640,7 +1600,6 @@ let saturate | CicRefine.AssertFailure s -> prerr_endline "FAILURE IN REFINE"; prerr_endline (Lazy.force s); - interactive_comparison context cic_proof_new cic_proof; assert false in if List.length newmetasenv_new <> 0 then