.depend{.opt} files changed

[helm.git] / matita / components / ng_disambiguation / nnumber_notation.mli

diff --git a/matita/components/ng_disambiguation/nnumber_notation.mli b/matita/components/ng_disambiguation/nnumber_notation.mli
index 91cba3b7c91490d5f1750c93475590a7063a9e14..dd0a6fbad29d106495f15f7ff99ee25612e89eeb 100644 (file)
--- a/matita/components/ng_disambiguation/nnumber_notation.mli
+++ b/matita/components/ng_disambiguation/nnumber_notation.mli
@@ -25,4 +25,4 @@
 
 (* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *)
 
-(* Works by side-effects only *)
+val ninterp_natural_number: string -> NCic.term