From: Ferruccio Guidi Date: Wed, 10 Jan 2007 14:30:22 +0000 (+0000) Subject: attributes now in the proof status: commit 3 X-Git-Tag: make_still_working~6530 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13c9f0ee2525769013a93333c4c8a65e603cc705;p=helm.git attributes now in the proof status: commit 3 --- diff --git a/helm/software/components/getter/http_getter_misc.ml b/helm/software/components/getter/http_getter_misc.ml index 45403effa..f7dffd066 100644 --- a/helm/software/components/getter/http_getter_misc.ml +++ b/helm/software/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/helm/software/components/hbugs/hbugs_tutors.ml b/helm/software/components/hbugs/hbugs_tutors.ml index 6a73e2cc2..ca6250262 100644 --- a/helm/software/components/hbugs/hbugs_tutors.ml +++ b/helm/software/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";