Hint Cut documentation and cleanup of printing (was duplicated and

inconsistent).

3 files changed, 12 insertions, 20 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index aa285fa98a..ee7b94b0d1 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -632,12 +632,7 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
 END
 
-
-let pr_hints_path_atom prc _ _ a =
-  match a with
-  | PathAny -> str"."
-  | PathHints grs ->
-    pr_sequence Printer.pr_global grs
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
   TYPED AS hints_path_atom
@@ -646,15 +641,7 @@ ARGUMENT EXTEND hints_path_atom
 | [ "*" ] -> [ PathAny ]
 END
 
-let pr_hints_path prc prx pry c =
-  let rec aux = function
-  | PathAtom a -> pr_hints_path_atom prc prx pry a
-  | PathStar p -> str"(" ++ aux p ++ str")*"
-  | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
-  | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
-  | PathEmpty -> str"ø"
-  | PathEpsilon -> str"ε"
-  in aux c
+let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 
 ARGUMENT EXTEND hints_path
   TYPED AS hints_path
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4ba9adafec..5630d20b5d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -382,15 +382,19 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
+let pp_hints_path_atom a =
+  match a with
+  | PathAny -> str"*"
+  | PathHints grs -> pr_sequence pr_global grs
+					   
 let rec pp_hints_path = function
-  | PathAtom (PathAny) -> str"."
-  | PathAtom (PathHints grs) -> pr_sequence pr_global grs
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathAtom pa -> pp_hints_path_atom pa
+  | PathStar p -> str "!(" ++ pp_hints_path p ++ str")"
   | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
   | PathOr (p, p') -> 
     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
-  | PathEmpty -> str"Ø"
-  | PathEpsilon -> str"ε"
+  | PathEmpty -> str"emp"
+  | PathEpsilon -> str"eps"
 
 let subst_path_atom subst p =
   match p with
diff --git a/tactics/hints.mli b/tactics/hints.mli
index af4d3d1f66..3a0521f665 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -70,6 +70,7 @@ type hints_path =
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 
 module Hint_db :