diff options
| author | Pierre-Marie Pédrot | 2020-07-13 14:55:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | 8076de05c67a4dabc99233d8e2b81809c28794e4 (patch) | |
| tree | 1ec6339fc0735fcc4609cf55b3aaae20b5e06026 /engine/eConstr.ml | |
| parent | d987a1575d4022d1e41a04a32836ac191380bd3f (diff) | |
Store the default instance in named_context_val.
This is not pretty but I do not see how to do this in a way that is both
backwards compatible and efficient.
Diffstat (limited to 'engine/eConstr.ml')
0 files changed, 0 insertions, 0 deletions