diff options
| author | Pierre-Marie Pédrot | 2020-12-24 17:21:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-20 10:54:34 +0200 |
| commit | 89c1ac8061dd044b1625a4b5f2ca65226f3826ee (patch) | |
| tree | a38cec6d12c23e51a9d51e240cce45250069f985 /plugins/ltac/tactic_debug.ml | |
| parent | b36fb9f68884090e5b06f9837da084395f519f96 (diff) | |
Preserve the context_val structure as much as possible in Logic.move.
Instead of going back and forth between the representations, we take
advantage of the fact we always leave context suffixes untouched.
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
0 files changed, 0 insertions, 0 deletions