X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b066b8ae09cafc5472a21c0bbc16b6a5625d7d21;hb=8752fac73a864c821b6954f0572bce2052924183;hp=d7343c98c1447c5831ace4066798c6828e37fd09;hpb=d7e33f1609c2d990eb52c3e30784a2aa7bdd9b32;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index d7343c98c..b066b8ae0 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -83,6 +83,7 @@ let tactic_of_ast ast =
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
       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:[])
@@ -139,7 +138,6 @@ let tactic_of_ast ast =
       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