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/funind/glob_term_to_relation.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/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0c45de4dc4..7c80b776a4 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -259,11 +259,8 @@ let mk_result ctxt value avoid = Some functions to deal with overlapping patterns **************************************************) -let coq_True_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") - -let coq_False_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") +let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type") +let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with @@ -957,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = assert false end | GApp(eq_as_ref,[ty; id ;rt]) - when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> let loc1 = rt.CAst.loc in let loc2 = eq_as_ref.CAst.loc in @@ -1078,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else new_b, Id.Set.add id id_to_exclude *) | GApp(eq_as_ref,[ty;rt1;rt2]) - when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> begin try @@ -1089,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc) ) b l |