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/Program/Tactics.v | 4 ++++ theories/Program/Wf.v | 4 ++++ 2 files changed, 8 insertions(+) (limited to 'theories/Program') 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. -- cgit v1.2.3