The proofContext method now returns the empty context when no proof is ongoing.

This behaviour is compatible with the behaviour of proofMetasenv

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index a94d8aecf90aa932f9863c59247b690560bf92e0..b0be9632df4609e5af5303ccbe5a56e422cb6068 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -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