diff options
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index bb1c0639e..345f46abf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -41,13 +41,15 @@ type subgoals = private { subgoals: goal list } type +'a sensitive (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *) -val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map +val eval : + 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> + 'a * Evd.evar_map * Declareops.side_effects (* monadic bind on sensitive expressions *) val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive (* monadic return on sensitive expressions *) -val return : 'a -> 'a sensitive +val return : 'a -> Declareops.side_effects -> 'a sensitive (* interpretation of "open" constr *) @@ -168,10 +170,10 @@ val here_list : goal list -> 'a -> 'a sensitive (* emulates List.map for functions of type [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating new evar_map to next definition *) -val list_map : (Evd.evar_map -> 'a -> 'b * Evd.evar_map) -> - 'a list -> - Evd.evar_map -> - 'b list *Evd.evar_map +val list_map : + (Evd.evar_map -> 'a -> 'b * Evd.evar_map * Declareops.side_effects) -> + 'a list -> Evd.evar_map -> + 'b list * Evd.evar_map * Declareops.side_effects list (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the |