Fix minor bug

coq/CertificateChecker.v

@@ -4,7 +4,7 @@ This function must be run on the daisy output.
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
-Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.PreconditionValidation.
+Require Import Daisy.IntervalValidation Daisy.ErrorValidation.
 
 Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs.

coq/IntervalValidation.v

@@ -5,6 +5,16 @@ Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
 Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps Daisy.PreconditionValidation.
 
+Import Lists.List.ListNotations.
+
+Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
+  match e with
+  |Const n => []
+  |Var v => []
+  |Param v => [v]
+  |Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
+  end.
+
 Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
   let (intv, _) := absenv e in
     match e with