The quoting function is now almost complete (in the sense that it can find

multiple solutions).

Since several solutions are observationally equal (i.e. they open the same
new set of goals), they are identified by the tactic. In case of multiple
non observationally equal solutions, the list of them is presented to the
user and the first one is randomically chosen. The user should be given
a possibility to choose.

Still todo: making the quoting function completely complete.

Note: the wf_unifty_to_subterm is now called twice. The first time is not
modulus delta conversion (the reasonable choice). The second time is modulus
delta conversion and the call is made iff the first call failed.
This is required by Ring that exploits the delta conversion ;-(


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6145 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions