X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fhbugs%2Fhbugs_tutors.ml;h=ca6250262ada9961628636b98bb56705af3efcb1;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hp=6a73e2cc283ec56c14b1f75ed16be3046c9dc4d4;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

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";