- decompose tactic: decomposable constants are now allowed (they are unfolded)

[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 366c0e264fe0d201fe071d6cf4b6fad8bf7f8fa0..98e57b5c4458e532334114deac4f1469f3e1fdc9 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -203,7 +203,8 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Inline (_,suri) -> sprintf "inline \"%s\"" suri
+  | Inline (_, suri, "") -> sprintf "inline \"%s\"" suri 
+  | Inline (_, suri, prefix) -> sprintf "inline \"%s\" \"%s\"" suri prefix 
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"