X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=b75192460135beeb4d2286c89ded2d0577af51c7;hb=7ad16d18416a08382d62747fce4a0ac18ee557e0;hp=a101747df7371d46fb54a54b0d84823faa2b4eaf;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index a101747df..b75192460 100644
--- 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)
@@ -154,8 +154,6 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
-    | Ast.Sort (`Type _) -> "Type"
-    | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
     | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
@@ -185,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"
@@ -281,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" 
@@ -324,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
@@ -340,7 +325,8 @@ let pp_obj pp_term = function
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)
-  | Env.StringValue s -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Ident s) -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Var s) -> sprintf "\"${ident %s}\"" s
   | Env.NumValue n -> n
   | Env.OptValue (Some v) -> "Some " ^ pp_value v
   | Env.OptValue None -> "None"
@@ -362,7 +348,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 -> "?"