From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Jan 2006 14:43:15 +0000 (+0000)
Subject: The proofContext method now returns the empty context when no proof is ongoing.
X-Git-Tag: make_still_working~7865
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcfba0fdd5fd4329986f8b717d908d3fb5b70103;p=helm.git

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 a94d8aecf..b0be9632d 100644
--- 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