]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/nCicBlob.ml
snaphost: supright almost done
[helm.git] / helm / software / components / ng_paramodulation / nCicBlob.ml
index a0fa80adab1bbff4f949c37b69d3734a79ba52e1..7cd4e5762f7d57c61c9caf179b9af64865ae4a1f 100644 (file)
@@ -63,7 +63,14 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     proof, sty
   ;;
 
-  let is_eq_predicate t = assert false;;
+  let eqP = 
+    let r = 
+      OCic2NCic.reference_of_oxuri 
+       (UriManager.uri_of_string 
+         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+    in
+    NCic.Const r
+  ;;
 
 
  end