From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 10 Jan 2007 14:30:22 +0000 (+0000)
Subject: attributes now in the proof status: commit 3
X-Git-Tag: 0.4.95@7852~671
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81a0d8630bef7e8f3d5f605fb9257cd2f99c935e;p=helm.git

attributes now in the proof status: commit 3
---

diff --git a/components/getter/http_getter_misc.ml b/components/getter/http_getter_misc.ml
index 45403effa..f7dffd066 100644
--- a/components/getter/http_getter_misc.ml
+++ b/components/getter/http_getter_misc.ml
@@ -279,7 +279,7 @@ let strip_suffix ~suffix s =
     let s_len = String.length s in
     let suffix_len = String.length suffix in
     let suffix_sub = String.sub s (s_len - suffix_len) suffix_len in
-    if suffix_sub <> suffix then raise (Invalid_argument "");
+    if suffix_sub <> suffix then raise (Invalid_argument "Http_getter_misc.strip_suffix");
     String.sub s 0 (s_len - suffix_len)
   with Invalid_argument _ ->
     raise (Invalid_argument "Http_getter_misc.strip_suffix")
diff --git a/components/hbugs/hbugs_tutors.ml b/components/hbugs/hbugs_tutors.ml
index 6a73e2cc2..ca6250262 100644
--- a/components/hbugs/hbugs_tutors.ml
+++ b/components/hbugs/hbugs_tutors.ml
@@ -113,13 +113,13 @@ let load_state (type_string, body_string, goal) =
   let (proof, goal) =
     prerr_endline "a2";
     (match CicParser.obj_of_xml tmp1 (Some tmp2) with
-    | Cic.CurrentProof (_,metasenv,bo,ty,_) ->  (* TODO il primo argomento e' una URI valida o e' casuale? *)
+    | Cic.CurrentProof (_,metasenv,bo,ty,attrs) ->  (* TODO il primo argomento e' una URI valida o e' casuale? *)
         prerr_endline "a3";
         let uri = UriManager.uri_of_string "cic:/foo.con" in
         prerr_endline "a4";
         typecheck_loaded_proof metasenv bo ty;
         prerr_endline "a5";
-        ((uri, metasenv, bo, ty), goal)
+        ((uri, metasenv, bo, ty, attrs), goal)
     | _ -> assert false)
   in
   prerr_endline "a6";