Remove non-DFSG contentsupstream/8.3.pl4+dfsg

3 files changed, 15 insertions, 13 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 86057b4b..095f50c6 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: cerrors.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -81,7 +81,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Syntax error: Undefined token.")
   | Lexer.Error (Bad_token s) ->
       hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
-  | Stdpp.Exc_located (loc,exc) ->
+  | Compat.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ explain_exn_default_aux anomaly_string report_fn exc)
@@ -156,8 +156,8 @@ let rec process_vernac_interp_error = function
   | Proof_type.LtacLocated (s,exc) ->
       EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
         Some (process_vernac_interp_error exc))
-  | Stdpp.Exc_located (loc,exc) ->
-      Stdpp.Exc_located (loc,process_vernac_interp_error exc)
+  | Compat.Exc_located (loc,exc) ->
+      Compat.Exc_located (loc,process_vernac_interp_error exc)
   | exc ->
       exc
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 9954ff56..551e5574 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: toplevel.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 open Pp
 open Util
@@ -274,7 +274,7 @@ let set_prompt prompt =
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+  | Compat.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
   | _ -> false
 
@@ -290,7 +290,7 @@ let print_toplevel_error exc =
   in
   let (locstrm,exc) =
     match exc with
-      | Stdpp.Exc_located (loc, ie) ->
+      | Compat.Exc_located (loc, ie) ->
           if valid_buffer_loc top_buffer dloc loc then
             (print_highlight_location top_buffer loc, ie)
           else
@@ -325,7 +325,7 @@ let parse_to_dot =
 let rec discard_to_dot () =
   try
     Gram.Entry.parse parse_to_dot top_buffer.tokens
-  with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
+  with Compat.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
     discard_to_dot()
 
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a7aef93f..de732618 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: vernac.ml 15025 2012-03-09 14:27:07Z glondu $ *)
 
 (* Parsing of vernacular. *)
 
@@ -41,14 +41,14 @@ let raise_with_file file exc =
     match re with
       | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
           ((b, f, loc), e)
-      | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
+      | Compat.Exc_located (loc, e) when loc <> dummy_loc ->
           ((false,file, loc), e)
-      | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
+      | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
   in
   raise (Error_in_file (file, inner, disable_drop inex))
 
 let real_error = function
-  | Stdpp.Exc_located (_, e) -> e
+  | Compat.Exc_located (_, e) -> e
   | Error_in_file (_, _, e) -> e
   | e -> e
 
@@ -206,7 +206,9 @@ let rec vernac_com interpfun (loc,com) =
 
     | VernacFail v ->
 	if not !just_parsing then begin try
-	  interp v; raise HasNotFailed
+	  (* If the command actually works, ignore its effects on the state *)
+	  States.with_state_protection
+	    (fun v -> interp v; raise HasNotFailed) v
 	with e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")