fixed paramodulation trnsition

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index d628af98dff7b237331bb4ca094087a9e41438ec..4c53f113bd9d0db4b7707d628a320be84f00dee8 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -80,8 +80,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
 =
   let module TAPp = GrafiteAstPp in
   let parsed_text_length = String.length parsed_text in
-  let loc, ex = 
-    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
   let initial_space,parsed_text =
    try
     let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
@@ -91,7 +89,9 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
    (* the code commented out adds the "select" command if needed *)
    initial_space,grafite_status,lexicon_status,[] in
-(*    match grafite_status.proof_status with
+(* let loc, ex = 
+    match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
+    match grafite_status.proof_status with
      | Incomplete_proof { stack = stack }
       when not (List.mem user_goal (Continuationals.head_goals stack)) ->
         let grafite_status =
@@ -755,9 +755,8 @@ object (self)
 
   method proofContext =
    match userGoal with
-      None -> assert false
-    | Some n ->
-       GrafiteTypes.get_proof_context self#grafite_status n
+      None -> []
+    | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
 
   method proofConclusion =
    match userGoal with
@@ -766,7 +765,7 @@ object (self)
        GrafiteTypes.get_proof_conclusion self#grafite_status n
 
   method stack = GrafiteTypes.get_stack self#grafite_status
-  method setGoal n = userGoal <- Some n
+  method setGoal n = userGoal <- n
   method goal = userGoal
 
   method eos =