diff options
Diffstat (limited to 'src/spl/Arithmetic.v')
| -rw-r--r-- | src/spl/Arithmetic.v | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/src/spl/Arithmetic.v b/src/spl/Arithmetic.v index 8ec41ab..05c999d 100644 --- a/src/spl/Arithmetic.v +++ b/src/spl/Arithmetic.v @@ -1,13 +1,9 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) @@ -16,8 +12,6 @@ (*** Spl -- a small checker for simplifications ***) -(* Add LoadPath ".." as SMTCoq. *) -(* Add LoadPath "../lia" as SMTCoq.lia. *) Require Import List PArray Bool Int63 ZMicromega. Require Import Misc State SMT_terms. Require Lia. @@ -52,7 +46,7 @@ Section Arith. Section Valid. - Variables (t_i : array typ_eqb) + Variables (t_i : array SMT_classes.typ_compdec) (t_func : array (Atom.tval t_i)) (ch_atom : Atom.check_atom t_atom) (ch_form : Form.check_form t_form) @@ -60,12 +54,14 @@ Section Arith. Local Notation interp_form_hatom := (Atom.interp_form_hatom t_i t_func t_atom). + Local Notation interp_form_hatom_bv := + (Atom.interp_form_hatom_bv t_i t_func t_atom). Local Notation rho := - (Form.interp_state_var interp_form_hatom t_form). + (Form.interp_state_var interp_form_hatom interp_form_hatom_bv t_form). Let wf_rho : Valuation.wf rho. - Proof. destruct (Form.check_form_correct interp_form_hatom _ ch_form); auto. Qed. + Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed. Hint Immediate wf_rho. |