X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=ade10ac8e2c88ab472dd3a3295dea1284e273bee;hb=ab2c76206276daec9863e1c385e8f27a7f899242;hp=794859369bbc62f593f392b80b73fcf63d6e19b7;hpb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;p=helm.git

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index 794859369..ade10ac8e 100644
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -38,10 +38,12 @@ let hide_coercions = ref true;;
 
 type cic_id = string
 
+(*
 type term_info =
   { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
     uri: (cic_id, NReference.reference) Hashtbl.t;
   }
+*)
 
 module IntMap = Map.Make(struct type t = int let compare = compare end);;
 module StringMap = Map.Make(String);;
@@ -79,7 +81,7 @@ class virtual status =
    method interp_db = match interp_db with None -> assert false | Some x -> x
    method set_interp_db v = {< interp_db = Some v >}
    method set_interp_status
-    : 'status. #g_status as 'status -> 'self
+    : 'status. (#g_status as 'status) -> 'self
     = fun o -> {< interp_db = Some o#interp_db >}#set_coercion_status o
    initializer
     interp_db <- Some (initial_db self)
@@ -185,7 +187,7 @@ let lookup_interpretations status ?(sorted=true) symbol =
           dsc, args, appl_pattern
       ) (StringMap.find symbol status#interp_db.interpretations)
     in
-    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+    if sorted then HExtlib.list_uniq (List.sort Stdlib.compare raw)
               else raw
   with Not_found -> raise Interpretation_not_found
 
@@ -432,7 +434,6 @@ let nmap_context0 status ~idref ~metasenv ~subst context =
 ;;
 
 let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) =
- let module K = Content in
  let nast_of_cic =
   nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
  let context' = nmap_context0 status ~idref ~metasenv ~subst context in