From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 3 Jun 2011 08:55:01 +0000 (+0000)
Subject: The pretty printer should never fail, even on fake inductive types used in
X-Git-Tag: make_still_working~2466
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98de36f4ccd98bdd9b49f396608e6f2600a23d3a;p=helm.git

The pretty printer should never fail, even on fake inductive types used in
patterns.
---

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index 84638ad6d..741cfa640 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 =