X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=038d75d9c7afd1862bfc0909ee002fd019d158b6;hb=3220eee6c3dd2968727c5c595d6ca78e89291b5f;hp=369a0fa281ac05e610f56d130b8cd477b4755724;hpb=cf8b1c25a0011ca2a8a856b39e046da33c451221;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 369a0fa28..038d75d9c 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -110,7 +110,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
 	  (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns status patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
-    | Ast.LetIn ((var,t2), t1, t3) ->
+    | Ast.LetIn ((var,_t2), t1, t3) ->
 (*       let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
         sprintf "let %s \\def %s in %s" (pp_term var)
 (*           (pp_term ~pp_parens:true t2) *)
@@ -251,8 +251,8 @@ and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
   | Ast.IdentVar s -> "ident " ^ s
   | Ast.TermVar (s,Ast.Self _) -> s
-  | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l 
-  | Ast.Ascription (t, n) -> assert false
+  | Ast.TermVar (_s,Ast.Level l) -> "term " ^string_of_int l 
+  | Ast.Ascription (_t, _n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
 let _pp_term = ref (pp_term ~pp_parens:false)