diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 0eae9b605..ebaa63267 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -403,6 +403,8 @@ module Goal : sig val env : 'a t -> Environ.env val sigma : 'a t -> Evd.evar_map + val raw_concl : 'a t -> Term.constr + (* [nf_enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) |