From: Alberto Griggio Date: Wed, 12 Oct 2005 12:37:36 +0000 (+0000) Subject: fixed a couple of bugs that broke tests... X-Git-Tag: V_0_7_2_3~215 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43c2a5068c1ff5f838e0558bb60c21e316cab852;p=helm.git fixed a couple of bugs that broke tests... --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 85ee885cb..0e5914b11 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -998,16 +998,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (* | _, _, (_, left, right, _), _, _ -> *) (* not (fst (CR.are_convertible context left right ugraph)) *) (* in *) - let _ = - let env = metasenv, context, ugraph in - debug_print - (lazy - (Printf.sprintf "end of superposition_right:\n%s\n" - (String.concat "\n" - ((List.map - (fun e -> "Positive " ^ - (Inference.string_of_equality ~env e)) (new1 @ new2)))))) - in let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index bf53f5cec..e4451769a 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1184,8 +1184,10 @@ let find_library_equalities dbd context status maxmeta = | C.Meta _ | C.Rel _ | C.Const _ -> false | C.Var _ -> true | C.Appl l -> List.exists has_vars l - | C.Prod (_, s, t) -> (has_vars s) || (has_vars t) - | _ -> assert false + | C.Prod (_, s, t) | C.Lambda (_, s, t) + | C.LetIn (_, s, t) | C.Cast (s, t) -> + (has_vars s) || (has_vars t) + | _ -> false in let rec aux newmeta = function | [] -> [], newmeta diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 181b4e1d9..00e266ce3 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -942,10 +942,10 @@ let apply_equality_to_goal env equality goal = let eqterm = C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in let gproof, gmetas, gterm = goal in - debug_print - (lazy - (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" - (string_of_equality equality) (CicPp.ppterm gterm))); +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *) +(* (string_of_equality equality) (CicPp.ppterm gterm))); *) try let subst, metasenv', _ = let menv = metasenv @ metas @ gmetas in @@ -1177,7 +1177,7 @@ let apply_to_goal env theorems ?passive active goal = in let r, s, l = if Inference.term_is_equality term then - let _ = debug_print (lazy "OK, is equality!!") in +(* let _ = debug_print (lazy "OK, is equality!!") in *) let rec appleq_a = function | [] -> false, [], [] | (Positive, equality)::tl ->