diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d2c05b913..17a1d3c34 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1303,6 +1303,7 @@ let status_changed lev (pbty,_,t1,t2) = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = try + assert(Evd.is_undefined evd evk1); let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = match kind_of_term t2 with | Evar (evk2,args2 as ev2) -> |