diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-03 17:29:20 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-03 17:29:20 +0100 |
| commit | 741d254d2d697cd9cd9da2edb9cd49462695092f (patch) | |
| tree | 00c7fe7c13dbeb25d0b85c4a39117c740cff1898 /src/common | |
| parent | c962467b9ab483beb17a4c264ee30242cdbafb7d (diff) | |
| download | vericert-741d254d2d697cd9cd9da2edb9cd49462695092f.tar.gz vericert-741d254d2d697cd9cd9da2edb9cd49462695092f.zip | |
Add externctrl props to HTLgen's st_prop
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Vericertlib.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 722edef..ae63e25 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -62,6 +62,13 @@ Ltac auto_hyp H := | H' : _ |- _ => solve [ apply H in H'; auto | auto ] end. +(** Specialize all hypotheses with a forall to a specific term *) +Tactic Notation "specialize_all" constr(v) := + let t := type of v in + repeat match goal with + | [H : (forall (x: t), _) |- _ ] => learn H; destruct H with v + end. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := |