From bcfba0fdd5fd4329986f8b717d908d3fb5b70103 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Jan 2006 14:43:15 +0000 Subject: [PATCH] The proofContext method now returns the empty context when no proof is ongoing. This behaviour is compatible with the behaviour of proofMetasenv --- helm/matita/matitaScript.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 -- 2.39.2