added a flag to do the check of alredy-proved-theorem

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index ce613ef7180fd1fdc5b68d9779f338e462393446..7aa31d33b6b3367ef8f632316129cb000da1fe90 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -77,10 +77,11 @@ let eval_with_engine status user_goal parsed_text st =
     match status.proof_status with
       | Incomplete_proof (_, goal) when goal <> user_goal ->
           goal_changed := true;
-          MatitaEngine.eval_ast status (goal_ast user_goal)
+          MatitaEngine.eval_ast 
+            ~do_heavy_checks:true status (goal_ast user_goal)
       | _ -> status
   in
-  let new_status = MatitaEngine.eval_ast status st in
+  let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in
   let new_aliases =
     match ex with
       | TA.Command (_, TA.Alias _)