diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2900.v | 28 |
2 files changed, 33 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) -> diff --git a/test-suite/bugs/closed/2900.v b/test-suite/bugs/closed/2900.v new file mode 100644 index 0000000000..8f4264e910 --- /dev/null +++ b/test-suite/bugs/closed/2900.v @@ -0,0 +1,28 @@ +(* Was raising stack overflow in 8.4 and assertion failed in future 8.5 *) +Set Implicit Arguments. + +Require Import List. +Require Import Coq.Program.Equality. + +(** Reflexive-transitive closure ( R* ) *) + +Inductive rtclosure (A : Type) (R : A-> A->Prop) : A->A->Prop := + | rtclosure_refl : forall x, + rtclosure R x x + | rtclosure_step : forall y x z, + R x y -> rtclosure R y z -> rtclosure R x z. + (* bug goes away if rtclosure_step is commented out *) + +(** The closure of the trivial binary relation [eq] *) + +Definition tr (A:Type) := rtclosure (@eq A). + +(** The bug *) + +Lemma bug : forall A B (l t:list A) (r s:list B), + length l = length r -> + tr (combine l r) (combine t s) -> tr l t. +Proof. + intros * E Hp. + (* bug goes away if [revert E] is called explicitly *) + dependent induction Hp. |