Commit a3a54a0f authored by Heiko Becker's avatar Heiko Becker
Browse files

Make certificate checker export return statements

parent 2232ce0f
......@@ -9,7 +9,7 @@ Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealR
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
......@@ -104,4 +104,4 @@ Proof.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
\ No newline at end of file
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