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

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 7cd4e5762..09399b326 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -27,10 +27,22 @@ 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.Meta (i,_), NCic.Meta (j,_) -> i-j
     | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
-    | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
+    | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+    | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+    | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+    | NCic.Appl _, NCic.Meta _ -> ~-1
+    | NCic.Meta _, NCic.Appl _ -> 1
     | _ -> assert false
   ;;
+  
+  let compare x y = 
+    if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 
+    else compare x y
+  ;;
 
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;