From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [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 Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- theories/Setoids/Setoid.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index af06bcf47e..43c8d9bc09 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -17,6 +17,8 @@ Export Morphisms.ProperNotations. Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. +Register Build_Setoid_Theory as plugins.setoid_ring.Build_Setoid_Theory. + Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. Proof. unfold Setoid_Theory in s. intros ; reflexivity. -- cgit v1.2.3