arithmetics for λδ

[helm.git] / matita / components / binaries / matex / anticipate.mli

diff --git a/matita/components/binaries/matex/anticipate.mli b/matita/components/binaries/matex/anticipate.mli
index e934bb4623141a04b3c17516abc339d53f3378b1..465cff23b0910b8dc48bd4be2f3ca55f21ece5c2 100644 (file)
--- a/matita/components/binaries/matex/anticipate.mli
+++ b/matita/components/binaries/matex/anticipate.mli
@@ -9,10 +9,6 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-val not_prop1: NCic.context -> NCic.term -> bool
-
-val not_prop2: NCic.context -> NCic.term -> bool
-
 val process_top_term: string -> NCic.term -> NCic.term
 
 val process_obj: NCic.obj_kind -> NCic.obj_kind