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 /theories/Program | |
| 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 'theories/Program')
| -rw-r--r-- | theories/Program/Tactics.v | 4 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index edbae6534a..001e1cfb01 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -237,6 +237,8 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i Definition fix_proto {A : Type} (a : A) := a. +Register fix_proto as program.tactic.fix_proto. + Ltac destruct_rec_calls := match goal with | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H @@ -331,3 +333,5 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; Obligation Tactic := program_simpl. Definition obligation (A : Type) {a : A} := a. + +Register obligation as program.tactics.obligation. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 6278798543..8479b9a2bb 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -32,6 +32,8 @@ Section Well_founded. Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + Register Fix_sub as program.wf.fix_sub. + (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) @@ -89,6 +91,8 @@ Section Measure_well_founded. Definition MR (x y: T): Prop := R (m x) (m y). + Register MR as program.wf.mr. + Lemma measure_wf: well_founded MR. Proof with auto. unfold well_founded. |