Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11

3 files changed, 9 insertions, 9 deletions

diff --git a/src/State.v b/src/State.v
index a3af611..4b0db6d 100644
--- a/src/State.v
+++ b/src/State.v
@@ -424,6 +424,13 @@ Module C.
     unfold valid, interp;destruct c;simpl; auto;discriminate.
   Qed.
 
+  Lemma Cinterp_neg rho cl :
+    interp rho (List.map Lit.neg cl) = negb (List.forallb (Lit.interp rho) cl).
+  Proof.
+    induction cl as [ |l cl IHcl]; auto.
+    simpl. now rewrite negb_andb, IHcl, Lit.interp_neg.
+  Qed.
+
 End C.
 
 
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 50cb0c0..f066b54 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1926,10 +1926,6 @@ Qed.
 Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b.
 Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed.
 
-  Axiom afold_left_xor : forall a,
-    afold_left bool int false xorb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
 Lemma eqb_spec : forall x y, (x == y) = true <-> x = y.
 Proof.
  split;auto using eqb_correct, eqb_complete.
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index 23aa979..cc956b3 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -345,9 +345,6 @@ Section CHECKER.
      match goal with |- context [Lit.interp rho ?x] => 
      destruct (Lit.interp rho x);trivial end.
 
-  Axiom Cinterp_neg : forall cl,
-     C.interp rho (map Lit.neg cl) = negb (forallb (Lit.interp rho) cl).  
-
   Lemma valid_check_BuildDef : forall l, C.valid rho (check_BuildDef l).
   Proof.
    unfold check_BuildDef,C.valid;intros l.
@@ -355,7 +352,7 @@ Section CHECKER.
      case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl;
        try (unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl;
             tauto_check).
-   - rewrite afold_left_and, Cinterp_neg;apply orb_negb_r.
+   - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r.
    - rewrite afold_left_or, orb_comm;apply orb_negb_r.
    - case_eq (PArray.length a == 0); auto using C.interp_true.
      intro Hl; simpl.
@@ -445,7 +442,7 @@ Section CHECKER.
    destruct (t_form.[Lit.blit l]);auto using C.interp_true;
    case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl;
    tauto_check.
-   - rewrite afold_left_and, Cinterp_neg, orb_false_r;trivial.
+   - rewrite afold_left_and, C.Cinterp_neg, orb_false_r;trivial.
    - rewrite afold_left_or, orb_false_r;trivial.
    - case_eq (PArray.length a == 0); auto using C.interp_true.
      intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl).