diff options
| author | Pierre-Marie Pédrot | 2018-10-11 14:27:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-11 14:27:29 +0200 |
| commit | aa5cdbd67b160417fe353a79393a89ed99481548 (patch) | |
| tree | 3104f09c8af83b2726530a4ed64175a3f179bad0 /theories/Program/Tactics.v | |
| parent | 96b30e352ff30b1fba4f11b278f22aa6db5871f9 (diff) | |
| parent | 8ac6145d5cc14823df48698a755d8adf048f026c (diff) | |
Merge PR #186: [RFC] Coqlib cleanup
Diffstat (limited to 'theories/Program/Tactics.v')
| -rw-r--r-- | theories/Program/Tactics.v | 4 |
1 files changed, 4 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. |