diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-05 17:44:45 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-05 17:44:45 +0000 |
| commit | 65eec025bc0b581fae1af78f18d1a8666b76e69b (patch) | |
| tree | 09a1d670468a2f141543c51a997f607f68eadef2 /proofs/goal.mli | |
| parent | 29301ca3587f2069278745df83ad46717a3108a9 (diff) | |
Moving side effects into evar_map. There was no reason to keep another
state out of one we were threading all the way along. This should be
safer, as one cannot forego side effects accidentally by manipulating
explicitly the [sigma] container.
Still, this patch raised the issue of badly used evar maps. There
is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the
fact it uses evar maps in an unorthodox way.
Likewise, that mean we have to revert all contrib patches that added
effect threading...
There was also a dubious use of side effects in their toplevel handling,
that duplicates them, leading to the need of a rather unsafe List.uniquize
afterwards. It should be investigaged.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index 267d26493..c07c7f28e 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -43,13 +43,13 @@ 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 * Declareops.side_effects + 'a * Evd.evar_map (* monadic bind on sensitive expressions *) val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive (* monadic return on sensitive expressions *) -val return : 'a -> Declareops.side_effects -> 'a sensitive +val return : 'a -> 'a sensitive (* interpretation of "open" constr *) @@ -171,9 +171,9 @@ val here_list : goal list -> 'a -> 'a sensitive [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 * Declareops.side_effects) -> + (Evd.evar_map -> 'a -> 'b * Evd.evar_map) -> 'a list -> Evd.evar_map -> - 'b list * Evd.evar_map * Declareops.side_effects list + 'b list * Evd.evar_map (* 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 |