diff options
| author | Hugo Herbelin | 2014-08-29 16:22:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-29 16:29:43 +0200 |
| commit | 029f850bceb1f68640fe7b703b0875ad02486691 (patch) | |
| tree | a96e55154df4399ffedf806b103a3d56473283eb /plugins/xml/xmlcommand.ml | |
| parent | e343fb550c3cd452f0646782edd39c9b7a5a992b (diff) | |
Not using a "cut" in descend_in_conjunctions induced more success. We
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions