arithmetics for λδ

[helm.git] / helm / software / matita / virtuals.ml

diff --git a/helm/software/matita/virtuals.ml b/helm/software/matita/virtuals.ml
index 4d7b91507e9250e9cbf199440edb1dd3b8a85021..229e780c28d8513951d1745e62595a7af7c642bb 100644 (file)
--- a/helm/software/matita/virtuals.ml
+++ b/helm/software/matita/virtuals.ml
@@ -56,4 +56,13 @@ let similar_symbols symbol =
   with Not_found -> []
 ;;
 
+let get_all_eqclass () =
+  let rc = ref [] in
+  Hashtbl.iter 
+    (fun k v ->
+      if not (List.mem v !rc) then
+        rc := v :: !rc)
+    classes;
+  !rc
+;;