]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_cic_content/interpretations.ml
Use of standard OCaml syntax
[helm.git] / matita / components / ng_cic_content / interpretations.ml
index 44d7751d500d74232d482a0e5117ddce72a6d066..ade10ac8e2c88ab472dd3a3295dea1284e273bee 100644 (file)
@@ -81,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)
@@ -434,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