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).

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.