diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:20 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:20 +0000 |
| commit | ea879916e09cd19287c831152d7ae2a84c61f4b0 (patch) | |
| tree | ba48057f7a5aa3fe160ba26313c5a74ec7a96162 /toplevel/vernac_classifier.mli | |
| parent | 07df7994675427b353004da666c23ae79444b0e5 (diff) | |
More Proofview.Goal.enter.
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.
This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.
This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac_classifier.mli')
0 files changed, 0 insertions, 0 deletions