5 files changed, 361 insertions, 54 deletions

diff --git a/math/coq/Makefile b/math/coq/Makefile
index 09ce880c5d97..f95ebd3f83ae 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -6,8 +6,7 @@
 #
 
 PORTNAME=	coq
-PORTVERSION=	8.3.2
-PORTREVISION=	1
+PORTVERSION=	8.3.3
 PORTEPOCH=	1
 CATEGORIES=	math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${COQVERSION}/files/ \
@@ -19,8 +18,6 @@ COMMENT=	Theorem prover based on lambda-C
 
 BUILD_DEPENDS=	camlp5:${PORTSDIR}/devel/ocaml-camlp5
 
-BROKEN=		does not build
-
 COQVERSION=	${PORTVERSION:R}pl${PORTVERSION:E}
 USE_OCAML=	yes
 USE_GMAKE=	yes
@@ -31,7 +28,6 @@ HAS_CONFIGURE=	yes
 CONFIGURE_ARGS=	--prefix ${PREFIX}
 CONFIGURE_ARGS+=--emacslib ${PREFIX}/share/emacs/site-lisp
 CONFIGURE_ARGS+=--opt
-PATCH_STRIP=	-p1
 
 .ifdef	NOPORTDOCS
 CONFIGURE_ARGS+=--with-doc none
diff --git a/math/coq/distinfo b/math/coq/distinfo
index e6c510d01234..43218988230b 100644
--- a/math/coq/distinfo
+++ b/math/coq/distinfo
@@ -1,2 +1,2 @@
-SHA256 (coq-8.3pl2.tar.gz) = b82b44ec585903b6bfadca02008eb5549cda46038c776ec115bc408c4e0f34f1
-SIZE (coq-8.3pl2.tar.gz) = 3760176
+SHA256 (coq-8.3pl3.tar.gz) = af259e9a723761327137018fdc0b98ada71095ff033b9e169d175d92b9537947
+SIZE (coq-8.3pl3.tar.gz) = 3859883
diff --git a/math/coq/files/ide-coqide.diff b/math/coq/files/ide-coqide.diff
deleted file mode 100644
index 34d8affdbd18..000000000000
--- a/math/coq/files/ide-coqide.diff
+++ /dev/null
@@ -1,47 +0,0 @@
---- coq-8.3/ide/coqide.ml	2010-07-24 17:57:30.000000000 +0200
-+++ coq-8.3/ide/coqide.ml	2010-11-04 23:09:29.000000000 +0100
-@@ -251,27 +251,29 @@
-     end
- 
- let do_if_not_computing text f x =
--  if Mutex.try_lock coq_computing then
--    let threaded_task () =
--      prerr_endline "Getting lock";
--      try
--        f x;
--        prerr_endline "Releasing lock";
--        Mutex.unlock coq_computing;
--      with e ->
--        prerr_endline "Releasing lock (on error)";
--        Mutex.unlock coq_computing;
--        raise e
--    in
-+  let threaded_task () =
-+    if Mutex.try_lock coq_computing then
-+      begin
-+        prerr_endline "Getting lock";
-+        try
-+          f x;
-+          prerr_endline "Releasing lock";
-+          Mutex.unlock coq_computing;
-+        with e ->
-+          prerr_endline "Releasing lock (on error)";
-+          Mutex.unlock coq_computing;
-+          raise e
-+      end
-+    else
-+     prerr_endline
-+      "Discarded order (computations are ongoing)"
-+  in
-       prerr_endline ("Launching thread " ^ text);
-       ignore (Glib.Timeout.add ~ms:300 ~callback:
-                   (fun () -> if Mutex.try_lock coq_computing
-                              then (Mutex.unlock coq_computing; false)
-                              else (pbar#pulse (); true)));
-       ignore (Thread.create threaded_task ())
--  else
--    prerr_endline
--      "Discarded order (computations are ongoing)"
- 
- (* XXX - 1 appel *)
- let kill_input_view i =
diff --git a/math/coq/files/patch-coq-camlp5-605 b/math/coq/files/patch-coq-camlp5-605
new file mode 100644
index 000000000000..a346759a8447
--- /dev/null
+++ b/math/coq/files/patch-coq-camlp5-605
@@ -0,0 +1,357 @@
+Fix compilation with camlp5 6.05
+Patch from the official coq svn repository (revision 15025)
+
+Index: checker/checker.ml
+===================================================================
+--- checker/checker.ml	(revision 15024)
++++ checker/checker.ml	(revision 15025)
+@@ -274,7 +274,7 @@
+ (*      let ctx = Check.get_env() in
+       hov 0
+         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
+-  | 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 exc)
+Index: lib/compat.ml4
+===================================================================
+--- lib/compat.ml4	(revision 15024)
++++ lib/compat.ml4	(revision 15025)
+@@ -15,6 +15,7 @@
+ IFDEF CAMLP5 THEN
+ module M = struct
+ type loc = Stdpp.location
++exception Exc_located = Ploc.Exc
+ let dummy_loc = Stdpp.dummy_loc
+ let make_loc = Stdpp.make_loc
+ let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
+@@ -26,6 +27,7 @@
+ end
+ ELSE IFDEF OCAML308 THEN
+ module M = struct
++exception Exc_located = Stdpp.Exc_located
+ type loc = Token.flocation
+ let dummy_loc = Token.dummy_loc
+ let make_loc loc = Token.make_loc loc
+@@ -45,6 +47,7 @@
+ end
+ ELSE
+ module M = struct
++exception Exc_located = Stdpp.Exc_located
+ type loc = int * int
+ let dummy_loc = (0,0)
+ let make_loc x = x
+@@ -59,6 +62,7 @@
+ END
+ 
+ type loc = M.loc
++exception Exc_located = M.Exc_located
+ let dummy_loc = M.dummy_loc
+ let make_loc = M.make_loc
+ let unloc = M.unloc
+Index: pretyping/pretype_errors.ml
+===================================================================
+--- pretyping/pretype_errors.ml	(revision 15024)
++++ pretyping/pretype_errors.ml	(revision 15025)
+@@ -45,7 +45,7 @@
+ 
+ let precatchable_exception = function
+   | Util.UserError _ | TypeError _ | PretypeError _
+-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
++  | Compat.Exc_located(_,(Util.UserError _ | TypeError _ |
+     Nametab.GlobalizationError _ | PretypeError _)) -> true
+   | _ -> false
+ 
+Index: pretyping/cases.ml
+===================================================================
+--- pretyping/cases.ml	(revision 15024)
++++ pretyping/cases.ml	(revision 15025)
+@@ -100,7 +100,7 @@
+   | h::t ->
+       try f h
+       with UserError _ | TypeError _ | PretypeError _
+-	| Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
++	| Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
+ 	    list_try_compile f t
+ 
+ let force_name =
+Index: pretyping/typeclasses_errors.ml
+===================================================================
+--- pretyping/typeclasses_errors.ml	(revision 15024)
++++ pretyping/typeclasses_errors.ml	(revision 15025)
+@@ -47,7 +47,7 @@
+       raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
+   | Some ev ->
+       let loc, kind = Evd.evar_source ev evd in
+-	raise (Stdpp.Exc_located (loc, TypeClassError
++	raise (Compat.Exc_located (loc, TypeClassError
+ 	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
+ 
+ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
+@@ -55,5 +55,5 @@
+ let rec unsatisfiable_exception exn =
+   match exn with
+   | TypeClassError (_, UnsatisfiableConstraints _) -> true
+-  | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
++  | Compat.Exc_located(_, e) -> unsatisfiable_exception e
+   | _ -> false
+Index: plugins/subtac/subtac_obligations.ml
+===================================================================
+--- plugins/subtac/subtac_obligations.ml	(revision 15024)
++++ plugins/subtac/subtac_obligations.ml	(revision 15025)
+@@ -485,8 +485,8 @@
+ 	      true
+ 	  else false
+ 	with
+-	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+-	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
++	| Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
++	| Compat.Exc_located(_, Refiner.FailError (_, s))
+ 	| Refiner.FailError (_, s) ->
+ 	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
+ 	| e -> false
+Index: toplevel/cerrors.ml
+===================================================================
+--- toplevel/cerrors.ml	(revision 15024)
++++ toplevel/cerrors.ml	(revision 15025)
+@@ -81,7 +81,7 @@
+       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 @@
+   | 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
+ 
+Index: toplevel/vernac.ml
+===================================================================
+--- toplevel/vernac.ml	(revision 15024)
++++ toplevel/vernac.ml	(revision 15025)
+@@ -41,14 +41,14 @@
+     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
+ 
+Index: toplevel/toplevel.ml
+===================================================================
+--- toplevel/toplevel.ml	(revision 15024)
++++ toplevel/toplevel.ml	(revision 15025)
+@@ -274,7 +274,7 @@
+ 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 @@
+   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 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()
+ 
+ 
+Index: tactics/extratactics.ml4
+===================================================================
+--- tactics/extratactics.ml4	(revision 15024)
++++ tactics/extratactics.ml4	(revision 15025)
+@@ -580,7 +580,7 @@
+     try 
+       Pretyping.Default.understand sigma env t_hole
+     with 
+-    | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
++    | Compat.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
+         resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
+   in
+   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
+Index: tactics/class_tactics.ml4
+===================================================================
+--- tactics/class_tactics.ml4	(revision 15024)
++++ tactics/class_tactics.ml4	(revision 15025)
+@@ -219,7 +219,7 @@
+ 
+ let rec catchable = function
+   | Refiner.FailError _ -> true
+-  | Stdpp.Exc_located (_, e) -> catchable e
++  | Compat.Exc_located (_, e) -> catchable e
+   | e -> Logic.catchable_exception e
+ 
+ let is_dep gl gls =
+Index: tactics/rewrite.ml4
+===================================================================
+--- tactics/rewrite.ml4	(revision 15024)
++++ tactics/rewrite.ml4	(revision 15025)
+@@ -1057,7 +1057,7 @@
+ 	      else tclIDTAC
+ 	    in tclTHENLIST [evartac; rewtac] gl
+ 	  with
+-	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
++	  | Compat.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+ 	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+ 	      Refiner.tclFAIL_lazy 0
+ 		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
+Index: tactics/tacinterp.ml
+===================================================================
+--- tactics/tacinterp.ml	(revision 15024)
++++ tactics/tacinterp.ml	(revision 15025)
+@@ -93,15 +93,15 @@
+ let catch_error call_trace tac g =
+   if call_trace = [] then tac g else try tac g with
+   | LtacLocated _ as e -> raise e
+-  | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
++  | Compat.Exc_located (_,LtacLocated _) as e -> raise e
+   | e ->
+     let (nrep,loc',c),tail = list_sep_last call_trace in
+-    let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
++    let loc,e' = match e with Compat.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
+     if tail = [] then
+       let loc = if loc = dloc then loc' else loc in
+-      raise (Stdpp.Exc_located(loc,e'))
++      raise (Compat.Exc_located(loc,e'))
+     else
+-      raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
++      raise (Compat.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+ 
+ (* Signature for interpretation: val_interp and interpretation functions *)
+ type interp_sign =
+@@ -1979,14 +1979,14 @@
+ 	VRTactic (catch_error trace tac goal)
+     | a -> a)
+   with
+-    | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
+-    | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
++    | FailError (0,s) | Compat.Exc_located(_, FailError (0,s))
++    | Compat.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
+ 	raise (Eval_fail (Lazy.force s))
+     | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+-    | Stdpp.Exc_located(s,FailError (lvl,s')) ->
+-	raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
+-    | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
+-	raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
++    | Compat.Exc_located(s,FailError (lvl,s')) ->
++	raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
++    | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
++	raise (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
+ 
+ (* Interprets the clauses of a recursive LetIn *)
+ and interp_letrec ist gl llc u =
+Index: ide/coq.ml
+===================================================================
+--- ide/coq.ml	(revision 15024)
++++ ide/coq.ml	(revision 15025)
+@@ -112,7 +112,7 @@
+     | _ -> true
+ 
+ let user_error_loc l s =
+-  raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
++  raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
+ 
+ type printing_state = {
+   mutable printing_implicit : bool;
+@@ -443,7 +443,7 @@
+ 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
+ 
+@@ -456,7 +456,7 @@
+   in
+   let (loc,exc) =
+     match exc with
+-      | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
++      | Compat.Exc_located (loc, ie) -> (Some loc),ie
+       | Error_in_file (s, (_,fname, loc), ie) -> None, ie
+       | _ -> dloc,exc
+   in
+Index: parsing/ppvernac.ml
+===================================================================
+--- parsing/ppvernac.ml	(revision 15024)
++++ parsing/ppvernac.ml	(revision 15025)
+@@ -781,7 +781,7 @@
+       (if i = 1 then mt() else int i ++ str ": ") ++
+       pr_raw_tactic tac
+       ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
+-      with UserError _|Stdpp.Exc_located _ -> mt())
++      with UserError _|Compat.Exc_located _ -> mt())
+ 
+   | VernacSolveExistential (i,c) ->
+       str"Existential " ++ int i ++ pr_lconstrarg c
+Index: proofs/refiner.ml
+===================================================================
+--- proofs/refiner.ml	(revision 15024)
++++ proofs/refiner.ml	(revision 15025)
+@@ -494,15 +494,15 @@
+ let catch_failerror e =
+   if catchable_exception e then check_for_interrupt ()
+   else match e with
+-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
+-  | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
++  | FailError (0,_) | Compat.Exc_located(_, FailError (0,_))
++  | Compat.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
+       check_for_interrupt ()
+   | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+-  | Stdpp.Exc_located(s,FailError (lvl,s')) ->
+-      raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
+-  | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s')))  ->
++  | Compat.Exc_located(s,FailError (lvl,s')) ->
++      raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
++  | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s')))  ->
+       raise
+-       (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
++       (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
+   | e -> raise e
+ 
+ (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
+Index: proofs/logic.ml
+===================================================================
+--- proofs/logic.ml	(revision 15024)
++++ proofs/logic.ml	(revision 15025)
+@@ -48,7 +48,7 @@
+ open Pretype_errors
+ 
+ let rec catchable_exception = function
+-  | Stdpp.Exc_located(_,e) -> catchable_exception e
++  | Compat.Exc_located(_,e) -> catchable_exception e
+   | LtacLocated(_,e) -> catchable_exception e
+   | Util.UserError _ | TypeError _
+   | RefinerError _ | Indrec.RecursionSchemeError _
diff --git a/math/coq/pkg-plist b/math/coq/pkg-plist
index 4b8412ee5429..8ae103300d81 100644
--- a/math/coq/pkg-plist
+++ b/math/coq/pkg-plist
@@ -130,6 +130,7 @@ lib/coq/lib/tries.cmi
 lib/coq/lib/unicodetable.cmi
 lib/coq/lib/util.cmi
 lib/coq/libcoqrun.a
+lib/coq/library/assumptions.cmi
 lib/coq/library/decl_kinds.cmi
 lib/coq/library/declare.cmi
 lib/coq/library/declaremods.cmi