Regular expression fixed to allow '-' into test names.

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 365bc9375f6d6a3a35ec45cb0d1da61e5e97ccfc..569b6839928467763c75a2f27886fbc3d6563af7 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -221,16 +221,26 @@ let pp_coercion uri do_composites arity =
    sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
      (if do_composites then "compounds" else "no compounds")
     
-let pp_command ~obj_pp = function
+let pp_command ~term_pp ~obj_pp = function
+  | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
+  | Default (_,what,uris) -> pp_default what uris
+  | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""
+  | Obj (_,obj) -> obj_pp obj
   | Qed _ -> "qed"
-  | Drop _ -> "drop"
+  | Relation (_,id,a,aeq,refl,sym,trans) ->
+     "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^
+     (match refl with
+         Some r -> " reflexivity proved by " ^ term_pp r
+       | None -> "") ^
+     (match sym with
+         Some r -> " symmetry proved by " ^ term_pp r
+       | None -> "") ^
+     (match trans with
+         Some r -> " transitivity proved by " ^ term_pp r
+       | None -> "")
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
-  | Obj (_,obj) -> obj_pp obj
-  | Default (_,what,uris) ->
-      pp_default what uris
 
 let rec pp_tactical ~term_pp ~lazy_term_pp =
   let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
@@ -271,7 +281,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
       pp_tactical ~lazy_term_pp ~term_pp tac
       ^ pp_tactical ~lazy_term_pp ~term_pp punct
   | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
-  | Command (_, cmd) -> pp_command ~obj_pp cmd ^ "."
+  | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function