urimanager removed

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

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 30abf348eda3b10e45941f096e31b50e26f9b7d7..e9209d5154e1faf27474ed193f7120472ebf022f 100644 (file)
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -104,7 +104,7 @@ let rec pp_term ?(pp_parens = true) t =
               sprintf " in %s%s" ty
               (match debug_printing, href_opt with
               | true, Some uri ->
-                  sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+                  sprintf "(i.e.%s)" (NReference.string_of_reference uri)
               | _ -> ""))        
          (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
@@ -183,7 +183,7 @@ and pp_pattern =
      let head_pp =
        head ^
        (match debug_printing, href with
-       | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+       | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
        | _ -> "")
      in
      sprintf "%s \\Rightarrow %s"
@@ -279,17 +279,6 @@ let pp_params pp_term = function
   | [] -> ""
   | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params)
       
-let pp_flavour = function
-  | `Definition -> "definition"
-  | `MutualDefinition -> assert false
-  | `Fact -> "fact"
-  | `Goal -> "goal"
-  | `Lemma -> "lemma"
-  | `Remark -> "remark"
-  | `Theorem -> "theorem"
-  | `Variant -> "variant"
-  | `Axiom -> "axiom"
-
 let pp_fields pp_term fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
@@ -322,11 +311,9 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
-    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body,_) ->
     sprintf "%s %s:\n %s\n%s"
-      (pp_flavour flavour)
+      (NCicPp.string_of_flavour flavour)
       name
       (pp_term typ)
       (match body with
@@ -360,7 +347,6 @@ let pp_env env =
       env)
 
 let rec pp_cic_appl_pattern = function
-  | Ast.UriPattern uri -> UriManager.string_of_uri uri
   | Ast.NRefPattern nref -> NReference.string_of_reference nref
   | Ast.VarPattern name -> name
   | Ast.ImplicitPattern -> "?"