diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-02 15:45:31 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-07 00:05:30 -0400 |
| commit | 3d77eaabd3aac64f1ab8b01a06b964b065889432 (patch) | |
| tree | 0726c5aafde263f8b53743169e91c7c2739ddc78 /.dir-locals.el | |
| parent | 76965f85cf742fb2fe9f75d7187da135fbd0eb57 (diff) | |
Factor out the compute bit of the compute notation in curve params
This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time
Diffstat (limited to '.dir-locals.el')
0 files changed, 0 insertions, 0 deletions