diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-10-23 19:31:52 +0200 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-10-23 15:00:57 -0400 |
| commit | acc4c4601efd15aa6e6d8624ce7f9ccc08792177 (patch) | |
| tree | 6f3442895df07d1ed497817ffd7856a219a52319 /src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v | |
| parent | 4b8ff5478b367cce44c87d5e3ecd94ff37593d57 (diff) | |
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Diffstat (limited to 'src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v')
0 files changed, 0 insertions, 0 deletions