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, 8 insertions, 1 deletions

diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 62bda6efd..963d61ca2 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -20,8 +20,15 @@ open Environ
 (** The "polyprop" optional argument is used by the extraction to
     disable "Prop-polymorphism", cf comment in [inductive.ml] *)
 
+(** The "lax" optional argument provides a relaxed version of
+    [get_type_of] that won't raise any anomaly but RetypeError instead *)
+
+type retype_error
+exception RetypeError of retype_error
+
 val get_type_of :
-  ?polyprop:bool -> ?refresh:bool -> env -> evar_map -> constr -> types
+  ?polyprop:bool -> ?refresh:bool -> ?lax:bool ->
+  env -> evar_map -> constr -> types
 
 val get_sort_of :
   ?polyprop:bool -> env -> evar_map -> types -> sorts