diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 13 |
4 files changed, 10 insertions, 9 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 94ec82029..621174aaa 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1532,7 +1532,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) reconsider_conv_pbs conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> - UnifFailure (evd,NotClean (ev1,t)) + UnifFailure (evd,NotClean (ev1,env,t)) | OccurCheckIn (evd,rhs) -> UnifFailure (evd,OccurCheck (evk1,rhs)) | MetaOccurInBodyInternal -> diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cad0beabf..e16d1206a 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,7 +14,7 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * constr + | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index cc1443162..b74ca1936 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -15,7 +15,7 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * constr + | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 15d6e29eb..90df17427 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -51,15 +51,16 @@ let contract3 env a b c = match contract env [a;b;c] with let contract4 env a b c d = match contract env [a;b;c;d] with | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false -let contract4_vect env a b c d v = - match contract env ([a;b;c;d] @ Array.to_list v) with - | env, a::b::c::d::l -> (env,a,b,c),d,Array.of_list l +let contract1_vect env a v = + match contract env (a :: Array.to_list v) with + | env, a::l -> env,a,Array.of_list l | _ -> assert false let contract3' env a b c = function | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d) - | NotClean ((evk,args),d) -> - let x,d,args = contract4_vect env a b c d args in x,NotClean((evk,args),d) + | NotClean ((evk,args),env',d) -> + let env',d,args = contract1_vect env' d args in + contract3 env a b c,NotClean((evk,args),env',d) | ConversionFailed (env',t1,t2) -> let (env',t1,t2) = contract2 env' t1 t2 in contract3 env a b c, ConversionFailed (env',t1,t2) @@ -264,7 +265,7 @@ let explain_unification_error env sigma p1 p2 = function spc () ++ str "(cannot define " ++ quote (pr_existential_key sigma evk) ++ strbrk " with term " ++ pr_lconstr_env env sigma rhs ++ strbrk " that would depend on itself)" - | NotClean ((evk,args),c) -> + | NotClean ((evk,args),env,c) -> let c = Evarutil.nf_evar sigma c in let args = Array.map (Evarutil.nf_evar sigma) args in spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key sigma evk) |