From c334523c4ff9b584ac108097fa6430e29f935e8f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Oct 2005 12:53:57 +0000 Subject: [PATCH] added goals_of_proof --- helm/ocaml/tactics/proofEngineTypes.ml | 3 +++ helm/ocaml/tactics/proofEngineTypes.mli | 3 +++ 2 files changed, 6 insertions(+) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 2e25e4a05..ed4a491e1 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -95,3 +95,6 @@ let apply_tactic t status = (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + +let goals_of_proof (_,metasenv,_,_) = List.map (fun (g,_,_) -> g) metasenv + diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index 63be26bb7..f45d681c1 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -72,3 +72,6 @@ val apply_tactic: tactic -> status -> proof * goal list (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + +val goals_of_proof: proof -> goal list + -- 2.39.2