X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=47b1ac0630ed7814bd7ad989e790cfbc5a29b35c;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=84638ad6dfa43e03cf473ff0e8d56b3d3b44a38c;hpb=ff3a27b1cbb969303ece080ef78cf53354545e5e;p=helm.git

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index 84638ad6d..47b1ac063 100644
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -305,6 +305,7 @@ let nast_of_cic0 status
                  [arg] -> idref (k ~context arg)
                | _ -> idref (Ast.Appl (List.map (k ~context) args))))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
+       (try
         let name = NUri.name_of_uri uri in
 (* CSC
         let uri_str = UriManager.string_of_uri uri in
@@ -351,6 +352,12 @@ let nast_of_cic0 status
           | `Term -> Some case_indty
         in
          idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+     with
+      NCicEnvironment.ObjectNotFound msg ->
+       idref (Ast.Case(k ~context te,Some ("NOT_FOUND: " ^ Lazy.force msg,None),
+       Some (k ~context outty),
+       (List.map (fun t -> Ast.Pattern ("????", None, []), k ~context t)
+         patterns))))
 ;;
 
 let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
@@ -632,16 +639,16 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) =
       n, is_ind, ty, List.map (build_constractor lno context) cl
    in
    match kind with
-      | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+      | NCic.Constant (_, n, xbo, ty, attrs) ->
 	 let ty = nast_of_cic ~context:[] ty in
          let xbo = match xbo with 
 	    | Some bo -> Some (nast_of_cic ~context:[] bo)
 	    | None    -> None
 	 in
-	 N.Theorem (flavour, n, ty, xbo, pragma)
-      | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->      
+	 N.Theorem (n, ty, xbo, attrs)
+      | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) ->      
          let captures, context = build_captures lno itl in
-	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src)
       | _ -> assert false  (* NCic.Fixpoint (is_rec, ifl, _) -> *)
 
 let nmap_obj status = with_idrefs nmap_obj0 status