[Pkg-ocaml-maint-commits] [why] 06/07: drop patch hashtbl

Ralf Treinen treinen at moszumanska.debian.org
Mon Apr 28 19:46:33 UTC 2014


This is an automated email from the git hooks/post-receive script.

treinen pushed a commit to branch master
in repository why.

commit 048b7d367cc8c89b4a24aba4f229ee293b8844e8
Author: Ralf Treinen <treinen at free.fr>
Date:   Mon Apr 28 21:31:30 2014 +0200

    drop patch hashtbl
---
 debian/changelog       |  1 +
 debian/patches/hashtbl | 56 --------------------------------------------------
 debian/patches/series  |  1 -
 3 files changed, 1 insertion(+), 57 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index 67b0484..9230d23 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -3,6 +3,7 @@ why (2.34-1) unstable; urgency=low
   * New upstream release.
   * Drop deprecated patches:
     - deprecated-or
+    - hashtbl
   * Bump build-dependency on frama-c to version 20140301+neon+dfsg-1.
   * Fix debian/tests/frama-c+jessie+alt-ergo: run why-config when there is
     no ${HOME}/.whyrc
diff --git a/debian/patches/hashtbl b/debian/patches/hashtbl
deleted file mode 100644
index d430202..0000000
--- a/debian/patches/hashtbl
+++ /dev/null
@@ -1,56 +0,0 @@
-Author: Jerry James <loganjerry at gmail.com >
-Description: fix type error with ocaml 4.01
-
-Index: why/jc/jc_annot_inference.ml
-===================================================================
---- why.orig/jc/jc_annot_inference.ml	2014-01-17 21:43:53.332548129 +0100
-+++ why/jc/jc_annot_inference.ml	2014-01-17 21:45:18.672822708 +0100
-@@ -84,7 +84,7 @@
- let unfolding_of_app app =
-   let f = app.jc_app_fun in
-   let _, term_or_assertion =
--    try Hashtbl.find Jc_typing.logic_functions_table f.jc_logic_info_tag
-+   try IntHashtblIter.find Jc_typing.logic_functions_table f.jc_logic_info_tag
-     with Not_found -> assert false
-   in
-   match term_or_assertion with
-@@ -2528,7 +2528,7 @@
- 	  in
- 	  let els = call.jc_call_args in
- 	  let _,_,fs,_ =
--            Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
-+            IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
-           in
-           (* Collect preconditions of functions called. *)
-           let reqa = fs.jc_fun_requires in
-@@ -3543,7 +3543,7 @@
-   (* Compute abstract value at function call *)
-   let curinvs = List.fold_left (ai_expr iaio abs) curinvs args in
-   let _f, _pos, spec, _body =
--    Hashtbl.find Jc_typing.functions_table f.jc_fun_info_tag
-+    IntHashtblIter.find Jc_typing.functions_table f.jc_fun_info_tag
-   in
- (*   begin match body with None -> () | Some body -> *)
- (*     if Jc_options.interprocedural then *)
-@@ -3732,9 +3732,9 @@
- 
-     (* Add global variables as abstract variables in [env]. *)
-     let globvars =
--      Hashtbl.fold (fun _tag (vi,_e) acc ->
--		      Vai.all_variables (new term_var vi) @ acc
--		   ) Jc_typing.variables_table []
-+      IntHashtblIter.fold (fun _tag (vi,_e) acc ->
-+			   Vai.all_variables (new term_var vi) @ acc
-+			  ) Jc_typing.variables_table []
-     in
-     let env = Environment.add env (Array.of_list globvars) [||] in
- 
-@@ -4164,7 +4164,7 @@
-     (fun fi ->
-        let fi, _, fs, slo =
- 	 try
--	   Hashtbl.find Jc_typing.functions_table fi.jc_fun_info_tag
-+	   IntHashtblIter.find Jc_typing.functions_table fi.jc_fun_info_tag
- 	 with Not_found -> assert false (* should never happen *)
-        in
-        match slo with
diff --git a/debian/patches/series b/debian/patches/series
index 6e2010c..d540ffa 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1,2 @@
-hashtbl
 atp-versions
 frama-c-versions

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git



More information about the Pkg-ocaml-maint-commits mailing list