diff options
| author | Arnaud Spiwack | 2014-09-08 09:48:47 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-08 10:58:23 +0200 |
| commit | 340bc24c06e0051b5e373dcdbe1691dfe9544054 (patch) | |
| tree | 3043920889e1ab03b51e003b54797ac7da803eb7 /plugins/xml/xmlcommand.mli | |
| parent | 9486c0bcaa39465ec254db72a13bd51313457ff1 (diff) | |
Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].
The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
Diffstat (limited to 'plugins/xml/xmlcommand.mli')
0 files changed, 0 insertions, 0 deletions