diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /plugins/extraction/ocaml.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r-- | plugins/extraction/ocaml.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 3cb3810c..1c29a9bc 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,7 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -203,7 +203,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 e when Errors.noncritical e -> apply (pp_global Term r)) + with e when CErrors.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 |