diff options
| author | Hugo Herbelin | 2014-06-13 10:33:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-13 12:08:33 +0200 |
| commit | c06fa8b4c16c35fe48039d5b13e181cca9ebbb51 (patch) | |
| tree | a56051d2986315eb2da48c605bd3cd894796e041 /plugins/xml/xmlcommand.ml | |
| parent | c272523bb9d89fe55d1636b48728e7938a8230dd (diff) | |
Check resolution of Metas turned into Evars by pose_all_metas_as_evars
in unification.ml in case prefix 'e' of "apply" and co is not given.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions