Bugs synchronisation pour gestion traduction des implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3884 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 20 insertions, 19 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1269ddfe3..5da98da62 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -140,16 +140,21 @@ let rec vernac_com interpfun (loc,com) =
              Options.v7_only := true;
              if !translate_file then msgnl (pr_comments !comments)
          | _ ->
-	     let f = match com with (* Pour gérer les implicites *)
-	       | VernacInductive _ -> States.with_heavy_rollback
+	     let protect = match com with (* Pour gérer les implicites *)
+	       | VernacFixpoint _ | VernacInductive _ ->
+		   fun f x -> 
+		     (let fs = States.freeze () in
+		     try let e = f x in States.unfreeze fs; e
+		     with e -> States.unfreeze fs; raise e)
 	       | _ -> fun f -> f in
              if !translate_file then
                msgnl
-		 (pr_comments !comments ++ hov 0 (f pr_vernac com) ++ sep_end)
+		 (pr_comments !comments ++ hov 0 (protect pr_vernac com) ++
+		  sep_end)
              else
 	       msgnl
                  (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         f pr_vernac com ++ sep_end)));
+                         protect pr_vernac com ++ sep_end)));
        comments := None;
        Format.set_formatter_out_channel stdout);
     interp com;
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index dfe934b7b..bd6648bb4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -538,25 +538,22 @@ let rec pr_vernac = function
       let pr_oneind (id,indpar,s,lc) =
         pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++
         pr_lconstr s ++ str" :=" ++ pr_constructor_list lc in
-      let p = prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l in
       hov 1
-        ((if f then str"Inductive" else str"CoInductive") ++ spc() ++ p)
+        ((if f then str"Inductive" else str"CoInductive") ++ spc() ++
+ 	 prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l)
 
   | VernacFixpoint recs ->
 
       (* Copie simplifiée de command.ml pour recalculer les implicites *)
       let sigma = Evd.empty
       and env0 = Global.env() in
-      let fs = States.freeze() in
-      (try 
-	List.iter
-          (fun (recname,_,arityc,_) -> 
-            let arity = Constrintern.interp_type sigma env0 arityc in
-            let _ = Declare.declare_variable recname
-	      (Lib.cwd(),Declare.SectionLocalAssum arity, Decl_kinds.IsAssumption Decl_kinds.Definitional) in ())
-          recs
-      with e ->
-	States.unfreeze fs; raise e);
+      List.iter
+        (fun (recname,_,arityc,_) -> 
+          let arity = Constrintern.interp_type sigma env0 arityc in
+          let _ = Declare.declare_variable recname
+	    (Lib.cwd(),Declare.SectionLocalAssum arity,
+	     Decl_kinds.IsAssumption Decl_kinds.Definitional) in ())
+        recs;
 
       let pr_onerec = function
         | (id,n,type_0,def0) ->
@@ -574,9 +571,8 @@ let rec pr_vernac = function
             pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
             ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in
-      let p = prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs in
-      States.unfreeze fs;
-      hov 1 (str"Fixpoint" ++ spc() ++ p)
+      hov 1 (str"Fixpoint" ++ spc() ++
+        prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint corecs ->
       let pr_onecorec (id,c,def) =