A fix for bug #1397:

 setoid_reflexivity may discover it is doing plain Leibniz stuff (see
 exception Optimize in setoid_replace), and falls back to the usual 
 reflexivity. Except that this one, due to the lack of delta-red, 
 refuses to handle the job, and gives it back to setoid_reflexivity: 
 a loop is born.

 quick fix for the moment: add some whd_betadeltaiota to reflexivity in 
 the special situation where reflexivity is called back by
 setoid_reflexivity.
 
 Similar issue & fix for symmetry, transitivity. 

 rewrite has potentially the same problem, but I can't manage to trigger
 a wild loop in practice. This code clearly deserves a closer look
 someday...




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

0 files changed, 0 insertions, 0 deletions