diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 8 |
2 files changed, 13 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 51d006e25..3045d66b8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -99,19 +99,19 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly ev evd t = +let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) - | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p | Lambda _ | LetIn _ -> false | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case _ -> false + | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -480,7 +480,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly (fst ev) i tR) then + if not (occur_rigidly ev i tR) then let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) @@ -1151,7 +1151,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 -> + | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c44903e8c..6e5ded152 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -613,7 +613,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si * substitution u1..uq. *) +exception MorePreciseOccurCheckNeeeded + let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = + if Evd.is_defined evd evk1 then + (* Some circularity somewhere (see e.g. #3209) *) + raise MorePreciseOccurCheckNeeeded; + let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in let evi1 = Evd.find_undefined evd evk1 in let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in @@ -1553,6 +1559,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = postpone_non_unique_projection env evd pbty ev sols rhs | NotEnoughInformationEvarEvar t -> add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd + | MorePreciseOccurCheckNeeeded -> + add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> |