Fix canonical structure resolution which was launched on the results of
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
Hurkens.v: Fix a syntax error.

Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
Adding a tclNEWGOALS primitive.
Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.

Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.