[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.29+dfsg-4-5-gd9b48a2

[Mehdi Dogguy]

The following commit has been merged in the master branch:
commit 31d1c6cd273ed00e47f3545a19436769f9702ce5
Author: Mehdi Dogguy <mehdi at dogguy.org>
Date:   Thu Dec 8 16:41:23 2011 +0100

    Update patches

diff --git a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
index c662fe6..d134d8d 100644
--- a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
+++ b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
@@ -7,10 +7,10 @@ Subject: Why 2.29 do support Coq 8.3
  1 files changed, 1 insertions(+), 1 deletions(-)
 
 diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index edaf366..8856081 100644
+index e298bcf..a2068e5 100644
 --- a/tools/dpConfig.ml
 +++ b/tools/dpConfig.ml
-@@ -199,7 +199,7 @@ let coq =
+@@ -221,7 +221,7 @@ let coq =
      version = "";
      version_switch = "-v";
      version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)";
diff --git a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
index d3f4192..a2b00b0 100644
--- a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
+++ b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
@@ -1,22 +1,22 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sat, 23 Apr 2011 20:07:20 +0200
-Subject: Mark alt-ergo 0.93 as compatible
+From: Mehdi Dogguy <mehdi at dogguy.org>
+Date: Thu, 8 Dec 2011 16:42:30 +0100
+Subject: Mark alt-ergo > 0.93 as compatible
 
 ---
  tools/dpConfig.ml |    2 +-
  1 files changed, 1 insertions(+), 1 deletions(-)
 
 diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index 8856081..fe72bf9 100644
+index a2068e5..8266412 100644
 --- a/tools/dpConfig.ml
 +++ b/tools/dpConfig.ml
 @@ -84,7 +84,7 @@ let alt_ergo =
      version = "";
      version_switch = "-version";
      version_regexp = ".*Ergo \\([^ ]*\\)";
--    versions_ok = ["0.91"; "0.92.1"; "0.92.2"];
-+    versions_ok = ["0.91"; "0.92.1"; "0.92.2"; "0.93"];
-     versions_old = ["0.8"; "0.9"];
+-    versions_ok = ["0.93"];
++    versions_ok = ["0.93"; "0.93.1"; "0.94"];
+     versions_old = ["0.8"; "0.9" ; "0.91"; "0.92.1"; "0.92.2" ];
      command = "alt-ergo";
      command_switches = "";
 -- 
diff --git a/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch b/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
index 2b22c73..54177f4 100644
--- a/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
+++ b/debian/patches/0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
@@ -7,7 +7,7 @@ Subject: Fix non-exhaustive pattern-matching in jc_annot_inference.ml
  1 files changed, 3 insertions(+), 3 deletions(-)
 
 diff --git a/jc/jc_annot_inference.ml b/jc/jc_annot_inference.ml
-index e7a1eae..d62a53c 100644
+index f4c9791..d9dbbd7 100644
 --- a/jc/jc_annot_inference.ml
 +++ b/jc/jc_annot_inference.ml
 @@ -148,7 +148,7 @@ let rec destruct_pointer t =
diff --git a/debian/patches/0004-Default-to-why2-for-jessie-atp.patch b/debian/patches/0004-Default-to-why2-for-jessie-atp.patch
new file mode 100644
index 0000000..31da14c
--- /dev/null
+++ b/debian/patches/0004-Default-to-why2-for-jessie-atp.patch
@@ -0,0 +1,22 @@
+From: Mehdi Dogguy <mehdi at dogguy.org>
+Date: Thu, 8 Dec 2011 16:46:48 +0100
+Subject: Default to why2 for -jessie-atp
+
+---
+ frama-c-plugin/jessie_options.ml |    2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/frama-c-plugin/jessie_options.ml b/frama-c-plugin/jessie_options.ml
+index 8e57656..8da0b66 100644
+--- a/frama-c-plugin/jessie_options.ml
++++ b/frama-c-plugin/jessie_options.ml
+@@ -175,7 +175,7 @@ module Atp =
+     (struct
+        let option_name = "-jessie-atp"
+        let module_name = "-jessie-atp"
+-       let default = "why3ml"
++       let default = "why2"
+        let arg_name = ""
+        let help = "use given automated theorem prover, among `alt-ergo', `cvc3', `simplify', `vampire', `yices' and `z3'. Use `goals' to simply generate goals in Why syntax."
+        let kind = `Tuning
+-- 
diff --git a/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
new file mode 100644
index 0000000..cdb459b
--- /dev/null
+++ b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
@@ -0,0 +1,22 @@
+From: Mehdi Dogguy <mehdi at dogguy.org>
+Date: Thu, 8 Dec 2011 17:08:36 +0100
+Subject: Fix Jc_annot_inference (use old_reg_pos)
+
+---
+ jc/jc_annot_inference.ml |    2 +-
+ 1 files changed, 1 insertions(+), 1 deletions(-)
+
+diff --git a/jc/jc_annot_inference.ml b/jc/jc_annot_inference.ml
+index d9dbbd7..08e66e4 100644
+--- a/jc/jc_annot_inference.ml
++++ b/jc/jc_annot_inference.ml
+@@ -491,7 +491,7 @@ let reg_annot ?id ?kind ?name ~pos ~anchor a =
+   in
+   Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
+   let formula = Format.flush_str_formatter () in
+-  let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
++  let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
+   new assertion_with ~mark:lab a
+ 
+ 
+-- 
diff --git a/debian/patches/series b/debian/patches/series
index c2c574c..3642552 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,3 +1,5 @@
 0001-Why-2.29-do-support-Coq-8.3.patch
 0002-Mark-alt-ergo-0.93-as-compatible.patch
 0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
+0004-Default-to-why2-for-jessie-atp.patch
+0005-Fix-Jc_annot_inference-use-old_reg_pos.patch

-- 
why packaging