From a479aa6e8dbd1dda1af2412f8c1e1ff40f0d5a0b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 12 Oct 2015 12:57:23 +0200
Subject: Fix rechecking of applications: it can be given ill-typed terms.
 Fixes math-classes.

---
 pretyping/evarsolve.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a2189d5e4f..754ad8f588 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -130,6 +130,8 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
 
 (* We retype applications to ensure the universe constraints are collected *)
 
+exception IllTypedInstance of env * types * types
+
 let recheck_applications conv_algo env evdref t =
   let rec aux env t =
     match kind_of_term t with
@@ -146,7 +148,7 @@ let recheck_applications conv_algo env evdref t =
 			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
 		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
-	 | _ -> assert false
+	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
      in aux 0 fty
     | _ ->
@@ -1134,8 +1136,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   else
     raise (CannotProject (evd,ev1'))
 
-exception IllTypedInstance of env * types * types
-
 let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
-- 
cgit v1.2.3