X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=ae9aa50270319ef2cedf6eee81c6e995633f1ede;hb=d97f69b313893900ca2d57544fcd200eb06ee286;hp=a98fb8e9d6cd70116d799750b65b06e285ba7bb4;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index a98fb8e9d..ae9aa5027 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -83,6 +83,12 @@ let pp_auto_params ~term_pp (univ, params) =
    else ""
 ;;
 
+let pp_just ~term_pp =
+ function
+    `Term term -> "exact " ^ term_pp term
+  | `Auto params -> pp_auto_params ~term_pp params
+;;
+
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
  let pp_terms = pp_terms ~term_pp in
  let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
@@ -113,7 +119,8 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | AutoBatch (_,params) -> "autobatch " ^ 
       pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
-  | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^
+  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
+      pp_tactic_pattern pattern ^
       pp_intros_specs "names " specs 
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
@@ -190,16 +197,16 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* Tattiche Aggiunte *)
   | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term 
   | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "("  ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
-  | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
-  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
+  | Bydone (_, just) ->  pp_just ~term_pp just ^ "done"
+  | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
   | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
-  | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
-  | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" 
+  | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
+  | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" 
   | RewritingStep (_, term, term1, term2, cont) -> 
       (match term with 
       | None -> " " 
@@ -281,15 +288,15 @@ let pp_default what uris =
   Printf.sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_coercion uri do_composites arity saturations=
+let pp_coercion ~term_pp t do_composites arity saturations=
    Printf.sprintf "coercion %s %d %d %s"
-    (UriManager.string_of_uri uri) arity saturations
+    (term_pp t) arity saturations
     (if do_composites then "" else "nocomposites")
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
-  | Coercion (_, uri, do_composites, i, j) ->
-     pp_coercion uri do_composites i j
+  | Coercion (_, t, do_composites, i, j) ->
+     pp_coercion ~term_pp t do_composites i j
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""