diff options
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. |