From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 19 Apr 2010 09:44:21 +0000 (+0000)
Subject: alpha_eq instead of pervasives.compare
X-Git-Tag: make_still_working~2919
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abdfd617eb0beb6961eea78e8f3b8cad73d43fde;hp=4682ca97a527e269be028e9f275c09c116511253;p=helm.git

alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index c1c7a9071..fb9ee6245 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -91,8 +91,8 @@ with type t = NCic.term and type input = NCic.term = struct
   ;;
   
   let compare x y = 
-    (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y  then 0 *)
-    if x = y  then 0
+    if NCicReduction.alpha_eq [] [] [] x y  then 0 
+    (* if x = y  then 0 *)
     else compare x y
   ;;