cicNotation* ==> notation*

[helm.git] / matita / components / content / interpretations.ml

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index 599a0704ecdda7d3c3ad01430c04b1f1b8f9918f..c7bfa576804b19621429f46f9556a4158b1db350 100644 (file)
--- a/matita/components/content/interpretations.ml
+++ b/matita/components/content/interpretations.ml
@@ -27,7 +27,7 @@
 
 open Printf
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 module Obj = LibraryObjects
 
 let debug = false
@@ -42,21 +42,6 @@ type term_info =
     uri: (Cic.id, UriManager.uri) Hashtbl.t;
   }
 
-let destroy_nat annterm =
-  let is_zero = function
-    | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
-    | _ -> false
-  in
-  let is_succ = function
-    | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
-    | _ -> false
-  in
-  let rec aux acc = function
-    | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
-    | t when is_zero t -> Some acc
-    | _ -> None in
-  aux 0 annterm
-
   (* persistent state *)
 
 let initial_level2_patterns32 () = Hashtbl.create 211
@@ -108,7 +93,7 @@ let instantiate32 term_info idrefs env symbol args =
         in
         let rec add_lambda t n =
           if n > 0 then
-            let name = CicNotationUtil.fresh_name () in
+            let name = NotationUtil.fresh_name () in
             Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
               Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
           else