X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=f329780633b423d2d0d626fdfd6ad18cb4b34156;hb=fafa203bb8521f516a0e87ef28d2cedccb72f795;hp=da3a730fb7831212b17c5f6ab09b012fefe78e2a;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index da3a730fb..f32978063 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -126,7 +126,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
-      | `Unfold what -> Tactics.unfold ~pattern ?what
+      | `Unfold what -> Tactics.unfold ~pattern what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->