- fwd concrete syntax fixed

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 43e2117cdb13470cb435776cd22c1420f6c68819..20d57ef9e5ab6cc63b92778d972fdf4f8a952bc5 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -72,6 +72,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyS (_, term) -> "applyS " ^ term_pp term
   | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
   | Auto _ -> "auto"
   | Assumption _ -> "assumption"
@@ -109,7 +110,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
        (lazy_term_pp term) (pp_tactic_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
-        (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+        (match idents with [] -> "" | idents -> " as " ^ pp_idents idents)
   | Generalize (_, pattern, ident) ->
      sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
@@ -129,7 +130,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
-        (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
+        (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
   | Reduce (_, kind, pat) ->