diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-06 20:09:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-07 00:56:23 +0200 |
| commit | ff81b7f1ffa594ab9f6fd174238b04cbbb1cfb71 (patch) | |
| tree | c5a19c7516d7707b8b7116545c7175fc021464a9 /pretyping | |
| parent | b44b68ec704df75f684e3393980f3518caf1a506 (diff) | |
Missing check of evar instantiation, resulting in missing constraints (bug from MathClasses).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index d15c5d00b..5f19ce30a 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 |