Retyping.get_type_of: a lax version raising no anomalies

 There are at least two situations (in Evarsolve and Pretyping)
 where Retyping.get_type_of may be called on ill-typed terms,
 leading to possible anomalies that used to be immediately catched
 and discarded. Instead, retyping.get_type_of now has an extra optional
 arg ~lax that makes it fail with a regular exception instead of
 anomalies.

 Of course, it would be best someday to be able to avoid using
 get_type_of on possibly ill-typed terms... If somebody wants to
 investigate this:

 - example that leads the get_type_of in Pretyping to a failure:
   test-suite/succes/ltac.v

 - example that leads the get_type_of in Evarsolve to a failure:
   MathClasses/implementations/list.v, a rewrite line 42 (* :-) *)
   cf bench failure on 2013-3-15.

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

0 files changed, 0 insertions, 0 deletions