X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=91746f210480f9eefae71b9cfde9aea198c238c0;hb=a09f5b76d65deba858fbba1a8b6e8481702d2166;hp=09399b3261b2d634352c54cc63b95614b898fb0b;hpb=01b628fc79155f545b283c1d095d8a2ffe00e0a1;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 09399b326..91746f210 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -18,7 +18,8 @@ module type NCicContext =
     val context : NCic.context
   end
 
-module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
+module NCicBlob(C : NCicContext) : Terms.Blob 
+with type t = NCic.term and type input = NCic.term = struct
 
   type t = NCic.term
 
@@ -26,7 +27,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
 
   let rec compare x y = 
     match x,y with
-    | NCic.Rel i, NCic.Rel j -> i-j
+    | NCic.Rel i, NCic.Rel j -> j-i
     | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
     | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
     | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
@@ -47,6 +48,8 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
 
+  type input = NCic.term
+
   let rec embed = function
     | NCic.Meta (i,_) -> Terms.Var i, [i]
     | NCic.Appl l ->
@@ -84,5 +87,4 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     NCic.Const r
   ;;
 
-
  end