diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 7e2d374d5b..7be8f6003b 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -335,17 +335,24 @@ end Eventually I'll try to remove it in favour of [Proofview.Goal] *) module Goal : sig - (* The type of goals *) - type t + (** The type of goals. The parameter type is a phantom argument indicating + whether the data contained in the goal has been normalized w.r.t. the + current sigma. If it is the case, it is flagged [ `NF ]. You may still + access the un-normalized data using {!assume} if you known you do not rely + on the assumption of being normalized, at your own risk. *) + type 'a t + + (** Assume that you do not need the goal to be normalized. *) + val assume : 'a t -> [ `NF ] t (* [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : t -> Term.constr - val hyps : t -> Context.named_context - val env : t -> Environ.env - val sigma : t -> Evd.evar_map + val concl : [ `NF ] t -> Term.constr + val hyps : [ `NF ] t -> Context.named_context + val env : 'a t -> Environ.env + val sigma : 'a t -> Evd.evar_map (* [lift_sensitive s k] applies [s] in each goal independently raising result [a] then continues with [k a]. *) @@ -354,15 +361,16 @@ module Goal : sig (* [enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) - val enter : (t -> unit tactic) -> unit tactic + val enter : ([ `NF ] t -> unit tactic) -> unit tactic + val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic (* compatibility: avoid if possible *) - val goal : t -> Goal.goal + val goal : [ `NF ] t -> Goal.goal (** [refresh g] updates the [sigma g] to the current value, may be useful with compatibility functions like [Tacmach.New.of_old] *) - val refresh_sigma : t -> t tactic + val refresh_sigma : 'a t -> 'a t tactic end (* The [NonLogical] module allows to execute side effects in tactics |