diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 24 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 2 |
2 files changed, 18 insertions, 8 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 35110552ab..2dc3e8a934 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -26,19 +26,29 @@ open Common (*S Part I: computing Coq environment. *) (***************************************) +(* FIXME: this is a Libobject hack that should be removed. *) +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> None + let toplevel_env () = let get_reference = function - | (_,kn), Lib.Leaf Libobject.AtomicObject o -> - let mp,l = KerName.repr kn in - begin match Libobject.object_tag o with - | "CONSTANT" -> + | (_,kn), Lib.Leaf Libobject.AtomicObject o -> + let mp,l = KerName.repr kn in + let handler = + DynHandle.add Declare.Internal.objConstant begin fun _ -> let constant = Global.lookup_constant (Constant.make1 kn) in Some (l, SFBconst constant) - | "INDUCTIVE" -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let inductive = Global.lookup_mind (MutInd.make1 kn) in Some (l, SFBmind inductive) - | _ -> None - end + end @@ + DynHandle.empty + in + handle handler o | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> let mp,l = KerName.repr kn in let modl = Global.lookup_module (MPdot (mp, l)) in diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 70c1077106..f6fbdaa958 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -164,7 +164,7 @@ let rawnum_of_r c = match DAst.get c with let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in let i = Bigint.to_string i in let se = if is_gr md glob_Rdiv then "-" else "" in - let e = se ^ Bigint.to_string e in + let e = "e" ^ se ^ Bigint.to_string e in s, { NumTok.int = i; frac = ""; exp = e } | _ -> raise Non_closed_number end |