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

1 files changed, 4 insertions, 4 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8ad2458af..712845f58 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -234,7 +234,7 @@ let _ = Errors.register_handler begin function
   | _ -> raise Errors.Unhandled
 end
 
-let return p t =
+let return p =
   if not (is_done p) then
     raise UnfinishedProof
   else if has_unresolved_evar p then
@@ -242,7 +242,7 @@ let return p t =
     raise HasUnresolvedEvar
   else
     let p = unfocus end_of_stack_kind p () in
-    Proofview.return p.proofview t
+    Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.proofview
 
@@ -271,10 +271,10 @@ module V82 = struct
     Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
 
   let top_goal p =
-    let { Evd.it=gls ; sigma=sigma; eff=eff } =
+    let { Evd.it=gls ; sigma=sigma; } =
 	Proofview.V82.top_goals p.proofview
     in
-    { Evd.it=List.hd gls ; sigma=sigma; eff=eff }
+    { Evd.it=List.hd gls ; sigma=sigma; }
 
   let top_evars p =
     Proofview.V82.top_evars p.proofview