diff options
| author | Hugo Herbelin | 2014-04-01 17:32:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-04-01 17:58:16 +0200 |
| commit | 36dd5dba9c7a86ef97e9f8bd96cbf6340098e2b7 (patch) | |
| tree | 3115235c0cea912a3e44a1f78a3e690cfd4647ab /pretyping | |
| parent | 68191dcce820a8135a84e716bddb7cf78476c360 (diff) | |
Fixing bug #2900 (evar/evar unif was supposed to be treated in
solve_simple_eqn but in case the second evar was hidden behind a
local variable, it arrived in evar_define and imitate, wrongly
assuming progress).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a96adcdd86..888f2fc8bd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1109,6 +1109,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress of (Id.t * evar_projection) list +exception NotEnoughInformationEvarEvar of constr exception OccurCheckIn of evar_map * constr exception MetaOccurInBodyInternal @@ -1187,7 +1188,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = with | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t | CannotProject filter' -> - assert !progress; + if not !progress then + raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = @@ -1311,6 +1313,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd ev sols rhs + | NotEnoughInformationEvarEvar t -> + add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> |