Commit b6c2abf8 authored by Joachim Bard's avatar Joachim Bard

making certificates compile

parent feb2e95d
......@@ -8,7 +8,8 @@ From Flover
Require Import Infra.RealRationalProps Environments TypeValidator
ResultChecker SubdivsChecker.
Require Export ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
Require Export List ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
Export ListNotations.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
......@@ -17,7 +18,7 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
match tMap with
|Succes Gamma =>
match subdivs with
| List.nil => ResultChecker e absenv P Qmap defVars Gamma
| [] => ResultChecker e absenv P Qmap defVars Gamma
| _ => SubdivsChecker e absenv P subdivs defVars Gamma
end
| _ => false
......
......@@ -10,8 +10,8 @@ From Flover
Require Import Infra.RealRationalProps Environments ExpressionSemantics SMTArith
TypeValidator FPRangeValidator ResultChecker.
Definition check_subdivs_step e defVars Gamma (b: bool) (p: analysisResult * precond) :=
let (A, P) := p in
Definition check_subdivs_step e defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
Definition check_subdivs e subdivs defVars Gamma :=
......
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