From 98de36f4ccd98bdd9b49f396608e6f2600a23d3a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 3 Jun 2011 08:55:01 +0000 Subject: [PATCH] The pretty printer should never fail, even on fake inductive types used in patterns. --- matita/components/ng_cic_content/interpretations.ml | 7 +++++++ 1 file changed, 7 insertions(+) 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 = -- 2.39.2