diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /plugins/extraction/ocaml.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r-- | plugins/extraction/ocaml.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 289b2a1d..4e8d8145 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -119,7 +119,8 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) - with _ -> (str "'a" ++ int i)) + with e when Errors.noncritical e -> + (str "'a" ++ int i)) | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r @@ -188,7 +189,7 @@ let rec pp_expr par env args = let args = list_skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with _ -> apply (pp_global Term r)) + with e when Errors.noncritical e -> apply (pp_global Term r)) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args |