From f066e0440f654917ca0969b4cbcf3a0d7be8a853 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 08:31:20 +0000 Subject: [PATCH] added #proofConclusion --- helm/matita/matitaScript.ml | 1 + helm/matita/matitaScript.mli | 1 + 2 files changed, 2 insertions(+) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 48cc9111b..e3dec088b 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -707,6 +707,7 @@ object (self) method proofStatus = MatitaMisc.get_proof_status self#status method proofMetasenv = MatitaMisc.get_proof_metasenv self#status method proofContext = MatitaMisc.get_proof_context self#status + method proofConclusion = MatitaMisc.get_proof_conclusion self#status method setGoal n = userGoal <- n method eos = diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 2cc559a3b..8c776685a 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -58,6 +58,7 @@ object method proofStatus: ProofEngineTypes.status (** @raise Statement_error *) method proofMetasenv: Cic.metasenv (** @raise Statement_error *) method proofContext: Cic.context (** @raise Statement_error *) + method proofConclusion: Cic.term (** @raise Statement_error *) method setGoal: int -> unit -- 2.39.2