diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-17 15:21:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 07:31:44 +0200 |
| commit | d76c6d9c92d8486ef4b672f9b44e5c6ea782d7ff (patch) | |
| tree | 97bd6b927186631693091b76091bb6fcb1b74eb9 /proofs | |
| parent | 08935581f9eccf7865adbf02d619bd41ba4fcdac (diff) | |
Proofview.mli: no more reference to Goal.goal.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 50e1d5eb8..7f070d006 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -328,7 +328,7 @@ end (*** Compatibility layer with <= 8.2 tactics ***) module V82 : sig - type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma val tactic : tac -> unit tactic (* normalises the evars in the goals, and stores the result in @@ -353,9 +353,9 @@ module V82 : sig (* Returns the open goals of the proofview together with the evar_map to interprete them. *) - val goals : proofview -> Goal.goal list Evd.sigma + val goals : proofview -> Evar.t list Evd.sigma - val top_goals : entry -> proofview -> Goal.goal list Evd.sigma + val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) val top_evars : entry -> Evd.evar list @@ -421,7 +421,7 @@ module Goal : sig val goals : [ `LZ ] t tactic list tactic (* compatibility: avoid if possible *) - val goal : [ `NF ] t -> Goal.goal + val goal : [ `NF ] t -> Evar.t end |