aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-17 20:46:20 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-17 20:46:20 +0000
commit7208928de37565a9e38f9540f2bfb1e7a3b877e6 (patch)
tree7d51cd24c406d349f4b7410c81ee66c210df49cd /plugins/extraction
parenta6dac9962929d724c08c9a74a8e05de06469a1a0 (diff)
More cleaning on Utils and CList. Some parts of the code being
peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml25
-rw-r--r--plugins/extraction/ocaml.ml4
2 files changed, 18 insertions, 11 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 9fe5606b9..2baea11a3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,17 +30,24 @@ let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
let mp,_,l = repr_kn kn in
- let seb = match Libobject.object_tag o with
- | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
- | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
- | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+ begin match Libobject.object_tag o with
+ | "CONSTANT" ->
+ let constant = Global.lookup_constant (constant_of_kn kn) in
+ Some (l, SFBconst constant)
+ | "INDUCTIVE" ->
+ let inductive = Global.lookup_mind (mind_of_kn kn) in
+ Some (l, SFBmind inductive)
+ | "MODULE" ->
+ let modl = Global.lookup_module (MPdot (mp, l)) in
+ Some (l, SFBmodule modl)
| "MODULE TYPE" ->
- SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
- | _ -> failwith "caught"
- in l,seb
- | _ -> failwith "caught"
+ let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+ Some (l, SFBmodtype modtype)
+ | _ -> None
+ end
+ | _ -> None
in
- SEBstruct (List.rev (map_succeed get_reference seg))
+ SEBstruct (List.rev (List.map_filter get_reference seg))
let environment_until dir_opt =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 78126bc16..826dcec02 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,7 @@ and pp_module_type params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp, sign) ->
push_visible mp params;
- let l = map_succeed pp_specif sign in
+ let l = List.map pp_specif sign in
pop_visible ();
str "sig " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +707,7 @@ and pp_module_expr params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEstruct (mp, sel) ->
push_visible mp params;
- let l = map_succeed pp_structure_elem sel in
+ let l = List.map pp_structure_elem sel in
pop_visible ();
str "struct " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++