diff options
Diffstat (limited to 'src/lia')
| -rw-r--r-- | src/lia/Lia.v | 5 | ||||
| -rw-r--r-- | src/lia/lia.ml | 1 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v index d8e89f3..dbd3b9c 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -1006,7 +1006,8 @@ Transparent build_z_atom. symmetry;apply Zgt_is_gt_bool. destruct t0;inversion H13;clear H13;subst. simpl. - symmetry;apply (Zeq_is_eq_bool (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). + apply (Z.eqb_eq (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). + Qed. Lemma build_formula_correct : @@ -1474,7 +1475,7 @@ Transparent build_z_atom. case_eq (vb <=? va); intros; subst. apply Zle_bool_imp_le in H2. apply Zle_bool_imp_le in H3. - apply Zeq_bool_neq in H. + apply Z.eqb_neq in H. (*pour la beauté du geste!*) lia. rewrite H3 in H1; simpl in H1; elim diff_true_false; trivial. rewrite H2 in H0; simpl in H1; elim diff_true_false; trivial. diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 589d59a..e5f2fe9 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -160,6 +160,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = failwith "Lia.smt_Form_to_coq_micromega_formula: wrong number of arguments for Fnot2" else smt_Form_to_coq_micromega_formula tbl l.(0) + | Fapp (Fforall _, _) -> assert false in if Form.is_pos l then v else N(v) |