diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 16:08:01 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-19 16:08:01 +0200 |
commit | 39fe4578c57795d5dadad08537c2cc49ba2636a1 (patch) | |
tree | 667f02dcf05a3861bdf377f633933fbe702455aa | |
parent | e273ff57ef82e81ab6b6309584a7d496ae4659c1 (diff) |
[proofs] Remove circular dependency from Proofview to Goal.
-rw-r--r-- | engine/proofview.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 530204501..957c9213c 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -25,7 +25,7 @@ type proofview new nearly identical function everytime. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) -val proofview : proofview -> Goal.goal list * Evd.evar_map +val proofview : proofview -> Evd.evar list * Evd.evar_map (** {6 Starting and querying a proof view} *) @@ -88,7 +88,7 @@ type focus_context new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -val focus_context : focus_context -> Goal.goal list * Goal.goal list +val focus_context : focus_context -> Evd.evar list * Evd.evar list (** [focus i j] focuses a proofview on the goals from index [i] to index [j] (inclusive, goals are indexed from [1]). I.e. goals @@ -148,7 +148,7 @@ type +'a tactic {!Logic_monad.TacticFailure}*) val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool*Goal.goal list*Goal.goal list) + * (bool*Evd.evar list*Evd.evar list) * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -304,12 +304,12 @@ val shelve : unit tactic (** Shelves the given list of goals, which might include some that are under focus and some that aren't. All the goals are placed on the shelf for later use (or being solved by side-effects). *) -val shelve_goals : Goal.goal list -> unit tactic +val shelve_goals : Evd.evar list -> unit tactic (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. Used by [shelve_unifiable]. *) -val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool +val unifiable : Evd.evar_map -> Evd.evar -> Evd.evar list -> bool (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -322,15 +322,15 @@ val guard_no_unifiable : Names.Name.t list option tactic (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) -val unshelve : Goal.goal list -> proofview -> proofview +val unshelve : Evd.evar list -> proofview -> proofview (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) -val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool +val depends_on : Evd.evar_map -> Evd.evar -> Evd.evar -> bool (** [with_shelf tac] executes [tac] and returns its result together with the set of goals shelved by [tac]. The current shelf is unchanged and the returned list contains only unsolved goals. *) -val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic +val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] is negative, then it puts the [n] last goals first.*) @@ -416,14 +416,14 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Goal.goal list -> unit tactic + val tclNEWGOALS : Evd.evar list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Goal.goal list -> unit tactic + val tclSETGOALS : Evd.evar list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Goal.goal list tactic + val tclGETGOALS : Evd.evar list tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic |