diff options
Diffstat (limited to 'community/coq')
| -rw-r--r-- | community/coq/PKGBUILD | 37 | ||||
| -rw-r--r-- | community/coq/camlp5-latest-fix.diff | 354 |
2 files changed, 0 insertions, 391 deletions
diff --git a/community/coq/PKGBUILD b/community/coq/PKGBUILD deleted file mode 100644 index 31077d16d..000000000 --- a/community/coq/PKGBUILD +++ /dev/null @@ -1,37 +0,0 @@ -# Maintainer: Thomas Dziedzic < gostrc at gmail > -# Contributor: George Giorgidze <giorgidze@gmail.com> - -pkgname=coq -pkgver=8.3pl4 -pkgrel=1 -pkgdesc='Formal proof management system.' -arch=('i686' 'x86_64') -url='http://coq.inria.fr/' -license=('GPL') -options=('!emptydirs') -depends=('gtk2' 'lablgtk2' 'ocaml') -makedepends=('camlp5-transitional' 'netpbm' 'hevea') -source=("http://coq.inria.fr/distrib/V${pkgver}/files/coq-${pkgver}.tar.gz") -md5sums=('88e2ce021b09eca207e3119d5202a695') - -build() { - cd coq-${pkgver} - - ./configure \ - -prefix '/usr' \ - -mandir '/usr/share/man' \ - -opt \ - -with-doc yes - - make world - - make doc-html -} - -package() { - cd coq-${pkgver} - - make COQINSTALLPREFIX=${pkgdir} install - - make COQINSTALLPREFIX=${pkgdir} install-doc-html -} diff --git a/community/coq/camlp5-latest-fix.diff b/community/coq/camlp5-latest-fix.diff deleted file mode 100644 index 80af1c924..000000000 --- a/community/coq/camlp5-latest-fix.diff +++ /dev/null @@ -1,354 +0,0 @@ -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 _ |