From ff81b7f1ffa594ab9f6fd174238b04cbbb1cfb71 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 6 Jul 2014 20:09:10 +0200
Subject: Missing check of evar instantiation, resulting in missing constraints
 (bug from MathClasses).

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

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index d15c5d00bd..5f19ce30a6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1119,7 +1119,9 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
     (* If instances are canonical, we solve the problem in linear time *)
     let sign = evar_filtered_context (Evd.find evd evk2) in
     let id_inst = inst_of_vars sign in
-    Evd.define evk2 (mkEvar(evk1,id_inst)) evd
+    let body = mkEvar(evk1,id_inst) in
+    let evd' = Evd.define evk2 body evd in
+      check_evar_instance evd' evk2 body g
   else
     let evd,ev1,ev2 =
       (* If an evar occurs in the instance of the other evar and the
-- 
cgit v1.2.3