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

1 files changed, 3 insertions, 2 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6818d84fe..83462d4c4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1040,9 +1040,10 @@ let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
+  (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
-    try Retyping.get_type_of evenv evd body
-    with e when Errors.noncritical e -> error "Ill-typed evar instance"
+    try Retyping.get_type_of ~lax:true evenv evd body
+    with Retyping.RetypeError _ -> error "Ill-typed evar instance"
   in
   match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd