]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaScript.ml
Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
[helm.git] / helm / matita / matitaScript.ml
index d628af98dff7b237331bb4ca094087a9e41438ec..a94d8aecf90aa932f9863c59247b690560bf92e0 100644 (file)
@@ -766,7 +766,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 =