Fix a bug in subst releaved by an OCaml warning.

3 files changed, 224 insertions, 3 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 06a9b317a2..b4c027382a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1730,20 +1730,22 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
-    let test (hyp,_,c) =
+    let select_equation_name (hyp,_,c) =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose c in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match kind_of_term x, kind_of_term y with
-        | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z))  ->
+        | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
+            Some hyp
+        | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
             Some hyp
         | _ ->
             None
       with Constr_matching.PatternMatchingFailure -> None
     in
     let hyps = Proofview.Goal.hyps gl in
-    List.rev (List.map_filter test hyps)
+    List.rev (List.map_filter select_equation_name hyps)
   in
 
   (* Second step: treat equations *)
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index 209b2bc26f..dbb9e09a43 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,6 +26,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -39,6 +52,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
   H1 : 0 = 1
   HA : True
   H2 : 0 = 2
@@ -52,6 +104,58 @@
   y, z : nat
   Hy : y = 0
   Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
   HA : True
   H3 : y = 3
   HB : True
@@ -75,6 +179,19 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -88,6 +205,45 @@
   True
 1 subgoal
   
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
   HA, HB : True
   H4 : 0 = 4
   H3 : 0 = 3
@@ -95,3 +251,55 @@
   H2 : 0 = 2
   ============================
   True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
index e48aa6bb28..91bdd03e02 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,4 +45,15 @@ Show.
 trivial.
 Qed.
 
+(* A bug revealed by OCaml 4.03 warnings *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was working *)
+Abort.
 
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+subst.
+Fail clear H. (* Was failing before fix *)
+Abort.