diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-11-05 10:32:47 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-11-05 10:32:47 +0100 |
| commit | 5e17f4a83b3fe5b8fdf58ab9643e33543d257bad (patch) | |
| tree | 84714cbe9b8e2392056532d9209766859478685f /src/common | |
| parent | 64a7fd889491bedffa3e3bcf130599c841c7008e (diff) | |
| download | vericert-dev/scheduling.tar.gz vericert-dev/scheduling.zip | |
Finish load proofdev/scheduling
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Vericertlib.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index da046f3..0310c19 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -82,6 +82,12 @@ Ltac destruct_match := Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. + Ltac destin x := + match type of x with + | context[match ?y with _ => _ end] => let DIN := fresh "DIN" in destruct y eqn:DIN + | _ => fail + end. + Ltac nicify_hypotheses := repeat match goal with | [ H : ex _ |- _ ] => inv H |