Merge branch 'ifExpr' of gitlab.mpi-sws.org:jbard/FloVer into ifExpr

coq/ErrorValidation.v

@@ -115,7 +115,13 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
              && validErrorbound e2 typeMap A (NatSet.add x dVars)
         then
           match FloverMap.find e1 A, FloverMap.find (Var Q x) A with
-          | Some (iv_e, err_e), Some (iv_x, err_x) => Qeq_bool err_e err_x
+          | Some (iv_e, err_e), Some (iv_x, err_x) =>
+            if (Qeq_bool err_e err_x)
+                 then
+                   match FloverMap.find e2 A with
+                   | Some (iv_e2, err_e2) => Qeq_bool err_e2 err
+                   | _,_ => false
+            else false
           | _,_ => false
           end
         else false