From: denes <??>
Date: Wed, 10 Jun 2009 08:46:55 +0000 (+0000)
Subject: Extended the equality case to non ground terms
X-Git-Tag: make_still_working~3889
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9ab150d29e4b7653f71085da477a1c81f7b7e131;p=helm.git

Extended the equality case to non ground terms
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 7c8a80995..8f0575a67 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -117,6 +117,11 @@ module Orderings (B : Terms.Blob) = struct
    * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
   let rec aux_ordering ?(head_only=false) t1 t2 =
     match t1, t2 with
+    (* We want to discard any identity equality. *
+     * If we give back XEQ, no inference rule    *
+     * will be applied on this equality          *)
+    | Terms.Var i, Terms.Var j when i = j ->
+	XEQ
     (* 1. *)
     | Terms.Var _, _
     | _, Terms.Var _ -> XINCOMPARABLE