X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=55736e862e2cba8aa5ee548a823691af3f7810aa;hb=6188c48d0ccbe5d8b7dbae9b8ff6de5bf984efa4;hp=910ad5204f5d427de157dab1996a274b4f2cff08;hpb=1beb5e1624ac1db045e36dff93d0cfafa6a70995;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 910ad5204..55736e862 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -36,7 +36,6 @@ let command_terminator = tactical_terminator
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind ~term_pp = function
-  | `Demodulate -> "demodulate"
   | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
@@ -99,6 +98,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       in
       let types = List.rev_map to_ident types in
       sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Demodulate _ -> "demodulate"
   | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ term_pp term ^
@@ -130,9 +130,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "intros%s%s"
         (match num with None -> "" | Some num -> " " ^ string_of_int num)
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
-  | LApply (_, level_opt, terms, term, ident_opt) -> 
-      sprintf "lapply %s%s%s%s" 
-        (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
+  | LApply (_, linear, level_opt, terms, term, ident_opt) -> 
+      sprintf "lapply %s%s%s%s%s" 
+        (if linear then " linear " else "")
+	(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 -> " as " ^ ident)
@@ -153,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+  
+  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"
@@ -181,11 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Search_pat (_, kind, pat) ->
-      sprintf "search %s \"%s\"" (pp_search_kind kind) pat
-  | Search_term (_, kind, term) ->
-      sprintf "search %s %s" (pp_search_kind kind) (term_pp term)
-  | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
 
 let pp_associativity = function