diff options
Diffstat (limited to 'plugins/micromega/QMicromega.v')
| -rw-r--r-- | plugins/micromega/QMicromega.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index b266a1ab8..ae22b0c78 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -80,7 +80,7 @@ Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := end. Lemma Qeval_expr_simpl : forall env e, - Qeval_expr env e = + Qeval_expr env e = match e with | PEc c => c | PEX j => env j @@ -179,7 +179,7 @@ Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool. Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool := - @tauto_checker (Formula Q) (NFormula Q) + @tauto_checker (Formula Q) (NFormula Q) Qnormalise Qnegate QWitness QWeakChecker f w. |