]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUtil.mli
hSqlite3.ml used create_fun_2 to define REGEXP.
[helm.git] / helm / software / components / cic / cicUtil.mli
index 9b1fecf0c25de2218a593884d8f92d9fbd4f17b5..de8c020952ac0262d774ef6c7ad2fff39d5d543a 100644 (file)
@@ -65,3 +65,4 @@ val mk_rels : int -> int -> Cic.term list
 val rehash_term: Cic.term -> Cic.term
 val rehash_obj: Cic.obj -> Cic.obj
 
+val alpha_equivalence: Cic.term -> Cic.term -> bool