X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b066b8ae09cafc5472a21c0bbc16b6a5625d7d21;hb=84505710c3e13bf06d7c3eeb87f924036c1896f1;hp=ae497fc12cbdd25db29b319643cfbe444d421aa0;hpb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ae497fc12..b066b8ae0 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -82,7 +82,8 @@ let tactic_of_ast ast =
       let user_types = List.rev_map to_type types in
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+  | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -96,8 +97,6 @@ let tactic_of_ast ast =
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
       let reduction =
         match reduction_kind with
-        | `Demodulate -> 
-            GrafiteTypes.command_error "demodulation can't be folded"
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
@@ -130,16 +129,15 @@ let tactic_of_ast ast =
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
-  | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+  | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
-        ~to_what what
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+        ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
-	 | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
 	 | `Normalize -> Tactics.normalize ~pattern
 	 | `Reduce -> Tactics.reduce ~pattern  
 	 | `Simpl -> Tactics.simpl ~pattern