From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 13 Aug 2009 15:45:49 +0000 (+0000)
Subject: Assert false do not allow to debug...
X-Git-Tag: make_still_working~3549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=651c5c55cba9ddbe592badc86b18502b83ecf580;p=helm.git

Assert false do not allow to debug...
---

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index eddac9746..6c7a6638a 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -89,7 +89,12 @@ let pp_just ~term_pp =
   | `Auto params -> pp_auto_params ~term_pp params
 ;;
 
-let rec pp_ntactic ~map_unicode_to_tex = function
+let rec pp_ntactic ~map_unicode_to_tex =
+ let term_pp = CicNotationPp.pp_term in
+ let lazy_term_pp = fun _ -> assert false in
+ let pp_tactic_pattern =
+  pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
+ function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
@@ -100,13 +105,15 @@ let rec pp_ntactic ~map_unicode_to_tex = function
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
   | NIntro (_,n) -> "#" ^ n
-  | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
+  | NRewrite (_,dir,n,where) -> "nrewrite " ^
+     (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
+     " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
   | NAuto (_,(l,flgs)) ->
       "nauto" ^ 
         (if l <> [] then (" by " ^
          (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
-  | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
+  | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
   | NDot _ -> "##."
   | NSemicolon _ -> "##;"
   | NBranch _ -> "##["
@@ -341,11 +348,6 @@ let pp_associativity = function
 
 let pp_precedence i = Printf.sprintf "with precedence %d" i
 
-let pp_dir_opt = function
-  | None -> ""
-  | Some `LeftToRight -> "> "
-  | Some `RightToLeft -> "< "
-
 let pp_default what uris = 
   Printf.sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))