1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index da3a730fb7831212b17c5f6ab09b012fefe78e2a..f329780633b423d2d0d626fdfd6ad18cb4b34156 100644 (file)
--- 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) ->