From 65eec025bc0b581fae1af78f18d1a8666b76e69b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 5 Oct 2013 17:44:45 +0000
Subject: 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
---
 printing/printer.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0e5d6721ed..2038fdeaa7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -388,7 +388,7 @@ let default_pr_subgoal n sigma =
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g; eff=Declareops.no_seff } in
+          let pg = default_pr_goal { sigma=sigma ; it=g; } in
           v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
 	       ++ str " is:" ++ cut () ++ pg)
 	else
@@ -439,7 +439,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
   in
   let print_multiple_goals g l =
     if pr_first then
-      default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } ++
+      default_pr_goal { it = g ; sigma = sigma; } ++
       pr_rec 2 l
     else 
       pr_rec 1 (g::l)
@@ -464,13 +464,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
                  str "You can use Grab Existential Variables.")
       end
   | [g],[] when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
 	str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
       )
   | [g],a::l when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
 	str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
@@ -556,7 +556,7 @@ let pr_goal_by_id id =
 	 ++ pr_goal gs)
   in
   try
-    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;eff=Declareops.no_seff})
+    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;})
   with Not_found -> error "Invalid goal identifier."
 
 (* Elementary tactics *)
-- 
cgit v1.2.3