diff options
| author | Emilio Jesus Gallego Arias | 2017-10-02 12:22:32 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-10 15:19:07 +0000 |
| commit | 8ac6145d5cc14823df48698a755d8adf048f026c (patch) | |
| tree | fa8bf650d111b828958ad7468fd0ec3b445d2305 /plugins/syntax/ascii_syntax.ml | |
| parent | ea38cc10b1b3d81e2346de6b95076733ef4fd7bb (diff) | |
[coqlib] Rebindable Coqlib namespace.
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 8ee6fbf036..94255bab6c 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -40,8 +40,7 @@ let ascii_kn = MutInd.make2 ascii_modpath ascii_label let path_of_Ascii = ((ascii_kn,0),1) let static_glob_Ascii = ConstructRef path_of_Ascii -let make_reference id = find_reference "Ascii interpretation" ascii_module id -let glob_Ascii = lazy (make_reference "Ascii") +let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii") open Lazy @@ -49,7 +48,7 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None)) :: (aux (n-1) (p/2)) in DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) @@ -67,8 +66,8 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux c = match DAst.get c with |