diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:27:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:46:39 +0200 |
| commit | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (patch) | |
| tree | a4a399bd1aeed5f047ccf1ad7c40573c7384e6aa /engine/proofview.mli | |
| parent | 112e974ec90b2afc51a7cffeba49e5777f3ea80f (diff) | |
| parent | 5dd690ee5975262d34d8dcc44191138c8d326f65 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index fae75f825..725445251 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -326,8 +326,9 @@ val unshelve : Goal.goal 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 -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [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 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -434,6 +435,9 @@ module Unsafe : sig and makes it unresolvable for type classes. *) val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) |