diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 19:35:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:02:32 +0200 |
| commit | fa1cb4a55262a1dced369ae6556265b968f4b9a3 (patch) | |
| tree | 77846b4238d1e7216a178a931f3454545f9e63be /pretyping | |
| parent | c12e158ad85da9d5e78026997ef6ca969c8ad3a6 (diff) | |
Fixing to #3209 (Not_found due to an occur-check cycle).
The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4084ee579..4a99246bb 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -600,7 +600,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 @@ -1542,6 +1548,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) -> |