Commit cbcaeb8b authored by Heiko Becker's avatar Heiko Becker

Change exported libs for certificate checker

parent 773e05ea
......@@ -9,7 +9,7 @@ From Flover
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment