X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2Finterpretations.ml;h=7e85d0fc1acd7fa061de8137f305b15e77288cc2;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=599a0704ecdda7d3c3ad01430c04b1f1b8f9918f;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index 599a0704e..7e85d0fc1 100644
--- a/matita/components/content/interpretations.ml
+++ b/matita/components/content/interpretations.ml
@@ -27,8 +27,7 @@
 
 open Printf
 
-module Ast = CicNotationPt
-module Obj = LibraryObjects
+module Ast = NotationPt
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -37,26 +36,13 @@ type interpretation_id = int
 
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
+type cic_id = string
+
 type term_info =
-  { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
-    uri: (Cic.id, UriManager.uri) Hashtbl.t;
+  { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
+    uri: (cic_id, NReference.reference) 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 +94,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
@@ -202,7 +188,7 @@ let remove_interpretation id =
 let init () = List.iter (fun f -> f []) !load_patterns32s
 
 let instantiate_appl_pattern 
-  ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern 
+  ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern 
 =
   let lookup name =
     try List.assoc name env
@@ -211,7 +197,6 @@ let instantiate_appl_pattern
       assert false
   in
   let rec aux = function
-    | Ast.UriPattern uri -> term_of_uri uri
     | Ast.NRefPattern nref -> term_of_nref nref
     | Ast.ImplicitPattern -> mk_implicit false
     | Ast.VarPattern name -> lookup name