diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-06 11:29:16 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-06 11:29:16 -0400 |
| commit | 5a0c4eb34708d2c85d91e6cb2c708ed16249e06d (patch) | |
| tree | 6988b67762b030d38b8941689cf00cc5fc6add1b /src/Experiments | |
| parent | 65ee6fbad9adc1e691c1f911cd084c60763046aa (diff) | |
stuck trying to figure out dependently typed continuation passing style
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index c0b6be25b..0f02000d0 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -18,16 +18,6 @@ Local Open Scope equiv_scope. Generalizable All Variables. -Local Ltac set_evars := - repeat match goal with - | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) - end. - -Local Ltac subst_evars := - repeat match goal with - | [ e := ?E |- _ ] => is_evar E; subst e - end. - Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)} {HP:Proper (RA==>Basics.impl) P} (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py)) |