Modify micromega/ZMicromega.v to compile with -mangle-names

1 files changed, 176 insertions, 168 deletions

diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index 1616b5a2a4..a4b631fc13 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -38,7 +38,7 @@ Ltac inv H := inversion H ; try subst ; clear H.
 Lemma eq_le_iff : forall x, 0 = x  <-> (0 <= x /\ x <= 0).
 Proof.
   intros.
-  split ; intros.
+  split ; intros H.
   - subst.
     compute. intuition congruence.
   - destruct H.
@@ -48,7 +48,7 @@ Qed.
 Lemma lt_le_iff : forall x,
     0 < x <-> 0 <= x - 1.
 Proof.
-  split ; intros.
+  split ; intros H.
   - apply Zlt_succ_le.
     ring_simplify.
     auto.
@@ -70,12 +70,13 @@ Lemma le_neg : forall x,
 Proof.
   intro.
   rewrite lt_le_iff.
-  split ; intros.
+  split ; intros H.
   - apply Znot_le_gt in H.
     apply Zgt_le_succ in H.
     rewrite le_0_iff in H.
     ring_simplify in H; auto.
-  - assert (C := (Z.add_le_mono _ _ _ _ H H0)).
+  - intro H0.
+    assert (C := (Z.add_le_mono _ _ _ _ H H0)).
     ring_simplify in C.
     compute in C.
     apply C ; reflexivity.
@@ -84,7 +85,7 @@ Qed.
 Lemma eq_cnf : forall x,
     (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0.
 Proof.
-  intros.
+  intros x.
   rewrite Z.eq_sym_iff.
   rewrite eq_le_iff.
   rewrite (le_0_iff x 0).
@@ -108,7 +109,7 @@ Proof.
   auto using Z.le_antisymm.
   eauto using Z.le_trans.
   apply Z.le_neq.
-  destruct (Z.lt_trichotomy n m) ; intuition.
+  apply Z.lt_trichotomy.
   apply Z.add_le_mono_l; assumption.
   apply Z.mul_pos_pos ; auto.
   discriminate.
@@ -160,18 +161,18 @@ Fixpoint Zeval_const  (e: PExpr Z) : option Z :=
 
 Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n.
 Proof.
-  destruct n.
+  intros r n; destruct n as [|p].
   reflexivity.
   simpl.
   unfold Z.pow_pos.
   replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring.
   generalize 1.
-  induction p; simpl ; intros ; repeat rewrite IHp ; ring.
+  induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring.
 Qed.
 
 Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.
 Proof.
-  induction e ; simpl ; try congruence.
+  intros env e; induction e ; simpl ; try congruence.
   reflexivity.
   rewrite ZNpower. congruence.
 Qed.
@@ -201,7 +202,7 @@ Lemma pop2_bop2 :
   forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
 Proof.
   unfold is_true.
-  destruct op ; simpl; intros.
+  intro op; destruct op ; simpl; intros q1 q2.
   - apply Z.eqb_eq.
   - rewrite <- Z.eqb_eq.
     rewrite negb_true_iff.
@@ -220,7 +221,7 @@ Definition Zeval_op2 (k: Tauto.kind) :  Op2 ->  Z -> Z -> Tauto.rtyp k:=
 Lemma Zeval_op2_hold : forall k op q1 q2,
     Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
 Proof.
-  destruct k.
+  intro k; destruct k.
   simpl ; tauto.
   simpl. apply pop2_bop2.
 Qed.
@@ -235,18 +236,18 @@ Definition Zeval_formula' :=
 
 Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.
 Proof.
-  destruct k ; simpl.
+  intros env k; destruct k ; simpl.
   - tauto.
-  - destruct f ; simpl.
-    rewrite <- Zeval_op2_hold with (k:=Tauto.isBool).
+  - intros f; destruct f ; simpl.
+    rewrite <- (Zeval_op2_hold Tauto.isBool).
     simpl. tauto.
 Qed.
 
 Lemma Zeval_formula_compat' : forall env f,  Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.
 Proof.
-  intros.
+  intros env f.
   unfold Zeval_formula.
-  destruct f.
+  destruct f as [Flhs  Fop Frhs].
   repeat rewrite Zeval_expr_compat.
   unfold Zeval_formula' ; simpl.
   unfold eval_expr.
@@ -343,7 +344,7 @@ Lemma Zunsat_sound : forall f,
     Zunsat f = true -> forall env, eval_nformula env f -> False.
 Proof.
   unfold Zunsat.
-  intros.
+  intros f H env ?.
   destruct f.
   eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto.
 Qed.
@@ -365,7 +366,7 @@ Lemma xnnormalise_correct :
   forall env f,
     eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.
 Proof.
-  intros.
+  intros env f.
   rewrite Zeval_formula_compat'.
   unfold xnnormalise.
   destruct f as [lhs o rhs].
@@ -375,18 +376,18 @@ Proof.
       generalize (   eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
                                  (fun x : N => x) (pow_N 1 Z.mul) env lhs);
       generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-                              (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros.
+                              (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0.
   - split ; intros.
-    + assert (z0 + (z - z0) = z0 + 0) by congruence.
+    + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence.
       rewrite Z.add_0_r in H0.
       rewrite <- H0.
       ring.
     + subst.
       ring.
-  - split ; repeat intro.
+  - split ; intros H H0.
     subst. apply H. ring.
     apply H.
-    assert (z0 + (z - z0) = z0 + 0) by congruence.
+    assert (z0 + (z - z0) = z0 + 0) as H1 by congruence.
     rewrite Z.add_0_r in H1.
     rewrite <- H1.
     ring.
@@ -396,11 +397,11 @@ Proof.
   - split ; intros.
     + apply Zle_0_minus_le; auto.
     + apply Zle_minus_le_0; auto.
-  - split ; intros.
+  - split ; intros H.
     + apply Zlt_0_minus_lt; auto.
     + apply Zlt_left_lt in H.
       apply H.
-  - split ; intros.
+  - split ; intros H.
     + apply Zlt_0_minus_lt ; auto.
     + apply Zlt_left_lt in H.
       apply H.
@@ -430,7 +431,7 @@ Ltac iff_ring :=
 Lemma xnormalise_correct : forall env f,
     (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f.
 Proof.
-  intros.
+  intros env f.
   destruct f as [e o]; destruct o eqn:Op; cbn - [psub];
     repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc;
       generalize (eval_pol env e) as x; intro.
@@ -458,11 +459,11 @@ Lemma cnf_of_list_correct :
   make_conj (fun x : NFormula Z => eval_nformula env x -> False) f.
 Proof.
   unfold cnf_of_list.
-  intros.
+  intros T tg f env.
   set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) =>
         if Zunsat x then acc else ((x, tg) :: nil) :: acc)).
   set (E := ((fun x : NFormula Z => eval_nformula env x -> False))).
-  induction f.
+  induction f as [|a f IHf].
   - compute.
     tauto.
   - rewrite make_conj_cons.
@@ -489,10 +490,10 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
 
 Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t.
 Proof.
-  intros.
+  intros T env t tg.
   rewrite <- xnnormalise_correct.
   unfold normalise.
-  generalize (xnnormalise t) as f;intro.
+  generalize (xnnormalise t) as f;intro f.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
     rewrite eval_cnf_ff.
@@ -519,10 +520,10 @@ Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
 Lemma xnegate_correct : forall env f,
     (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f.
 Proof.
-  intros.
+  intros env f.
   destruct f as [e o]; destruct o eqn:Op; cbn - [psub];
     repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc;
-      generalize (eval_pol env e) as x; intro.
+      generalize (eval_pol env e) as x; intro x.
   - tauto.
   - rewrite eq_cnf.
     destruct (Z.eq_decidable x 0);tauto.
@@ -533,10 +534,10 @@ Qed.
 
 Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t.
 Proof.
-  intros.
+  intros T env t tg.
   rewrite <- xnnormalise_correct.
   unfold negate.
-  generalize (xnnormalise t) as f;intro.
+  generalize (xnnormalise t) as f;intro f.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
     rewrite eval_cnf_tt.
@@ -569,10 +570,10 @@ Require Import Znumtheory.
 Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b.
 Proof.
   unfold ceiling.
-  intros.
+  intros a b H.
   apply Zdivide_mod in H.
   case_eq (Z.div_eucl a b).
-  intros.
+  intros z z0 H0.
   change z with (fst (z,z0)).
   rewrite <- H0.
   change (fst (Z.div_eucl a b)) with (Z.div a b).
@@ -642,12 +643,12 @@ Definition isZ0 (x:Z) :=
 
 Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.
 Proof.
-  destruct x ; simpl ; intuition congruence.
+  intros x; destruct x ; simpl ; intuition congruence.
 Qed.
 
 Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0.
 Proof.
-  destruct x ; simpl ; intuition congruence.
+  intros x; destruct x ; simpl ; intuition congruence.
 Qed.
 
 Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1.
@@ -682,8 +683,8 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop :=
 Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p  ->
   forall env, eval_pol env p =  a * eval_pol env (Zdiv_pol p a).
 Proof.
-  intros until 2.
-  induction H0.
+  intros a p H H0.
+  induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j].
   (* Pc *)
   simpl.
   intros.
@@ -702,7 +703,7 @@ Qed.
 
 Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
 Proof.
-  induction p. 1-2: easy.
+  intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy.
   simpl.
   case_eq (Zgcd_pol p1).
   case_eq (Zgcd_pol p3).
@@ -715,7 +716,7 @@ Qed.
 
 Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) ->  Zdivide_pol y p.
 Proof.
-  intros.
+  intros p x y H H0.
   induction H.
   constructor.
   apply Z.divide_trans with (1:= H0) ; assumption.
@@ -725,7 +726,7 @@ Qed.
 
 Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
 Proof.
-  induction p ; constructor ; auto.
+  intros p; induction p as [c| |]; constructor ; auto.
   exists c. ring.
 Qed.
 
@@ -744,19 +745,19 @@ Lemma Zdivide_pol_sub : forall p a b,
   Zdivide_pol a (PsubC Z.sub p b) ->
    Zdivide_pol (Z.gcd a b) p.
 Proof.
-  induction p.
+  intros p; induction p as [c|? p IHp|p ? ? ? IHp2].
   simpl.
-  intros. inversion H0.
+  intros a b H H0. inversion H0.
   constructor.
   apply Zgcd_minus ; auto.
-  intros.
+  intros ? ? H H0.
   constructor.
   simpl in H0. inversion H0 ; subst; clear H0.
   apply IHp ; auto.
-  simpl. intros.
+  simpl. intros a b H H0.
   inv H0.
   constructor.
-  apply Zdivide_pol_Zdivide with (1:= H3).
+  apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)).
   destruct (Zgcd_is_gcd a b) ; assumption.
   apply IHp2 ; assumption.
 Qed.
@@ -765,15 +766,15 @@ Lemma Zdivide_pol_sub_0 : forall p a,
   Zdivide_pol a (PsubC Z.sub p 0) ->
    Zdivide_pol a p.
 Proof.
-  induction p.
+  intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2].
   simpl.
-  intros. inversion H.
+  intros ? H. inversion H.
   constructor. rewrite Z.sub_0_r in *. assumption.
-  intros.
+  intros ? H.
   constructor.
   simpl in H. inversion H ; subst; clear H.
   apply IHp ; auto.
-  simpl. intros.
+  simpl. intros ? H.
   inv H.
   constructor. auto.
   apply IHp2 ; assumption.
@@ -783,9 +784,9 @@ Qed.
 Lemma Zgcd_pol_div : forall p g c,
   Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).
 Proof.
-  induction p ; simpl.
+  intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl.
   (* Pc *)
-  intros. inv H.
+  intros ? ? H. inv H.
   constructor.
   exists 0. now ring.
   (* Pinj *)
@@ -793,28 +794,28 @@ Proof.
   constructor.  apply IHp ; auto.
   (* PX *)
   intros g c.
-  case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros.
+  case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1.
   inv H1.
   unfold ZgcdM at 1.
   destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
   destruct HH1 as [HH1 HH1'] ; rewrite HH1'.
   constructor.
-  apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2).
+  apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)).
   unfold ZgcdM.
   destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
-  destruct HH2.
+  destruct HH2 as [H1 H2].
   rewrite H2.
   apply Zdivide_pol_sub ; auto.
   apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le.
-  destruct HH2. rewrite H2.
+  destruct HH2 as [H1 H2]. rewrite H2.
   apply Zdivide_pol_one.
   unfold ZgcdM in HH1. unfold ZgcdM.
   destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
-  destruct HH2. rewrite H2 in *.
+  destruct HH2 as [H1 H2]. rewrite H2 in *.
   destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto.
-  destruct HH2. rewrite H2.
+  destruct HH2 as [H1 H2]. rewrite H2.
   destruct (Zgcd_is_gcd 1  z); auto.
-  apply Zdivide_pol_Zdivide with (x:= z).
+  apply (Zdivide_pol_Zdivide _ z).
   apply (IHp2 _ _ H); auto.
   destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto.
   constructor. apply Zdivide_pol_one.
@@ -873,7 +874,7 @@ Definition is_pol_Z0 (p : PolC Z) : bool :=
 Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0.
 Proof.
   unfold is_pol_Z0.
-  destruct p ; try discriminate.
+  intros p; destruct p as [z| |]; try discriminate.
   destruct z ; try discriminate.
   reflexivity.
 Qed.
@@ -915,8 +916,8 @@ Fixpoint max_var (jmp : positive) (p : Pol Z) : positive :=
 Lemma pos_le_add : forall y x,
     (x <= y + x)%positive.
 Proof.
-  intros.
-  assert  ((Z.pos x) <= Z.pos (x + y))%Z.
+  intros y x.
+  assert  ((Z.pos x) <= Z.pos (x + y))%Z as H.
   rewrite <- (Z.add_0_r (Zpos x)).
   rewrite <- Pos2Z.add_pos_pos.
   apply Z.add_le_mono_l.
@@ -929,10 +930,10 @@ Qed.
 Lemma max_var_le : forall p v,
     (v <= max_var v p)%positive.
 Proof.
-  induction p; simpl.
+  intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl.
   - intros.
     apply Pos.le_refl.
-  - intros.
+  - intros v.
     specialize (IHp (p+v)%positive).
     eapply Pos.le_trans ; eauto.
     assert (xH + v <= p + v)%positive.
@@ -942,7 +943,7 @@ Proof.
     }
     eapply Pos.le_trans ; eauto.
     apply pos_le_add.
-  - intros.
+  - intros v.
     apply Pos.max_case_strong;intros ; auto.
     specialize (IHp2 (Pos.succ v)%positive).
     eapply Pos.le_trans ; eauto.
@@ -951,10 +952,10 @@ Qed.
 Lemma max_var_correct : forall p j v,
     In v (vars j p) -> Pos.le v (max_var j p).
 Proof.
-  induction p; simpl.
+  intros p; induction p; simpl.
   - tauto.
   - auto.
-  - intros.
+  - intros j v H.
     rewrite in_app_iff in H.
     destruct H as [H |[ H | H]].
     + subst.
@@ -980,7 +981,7 @@ Section MaxVar.
       (v <= acc ->
        v <= fold_left F l acc)%positive.
   Proof.
-    induction l ; simpl ; [easy|].
+    intros l; induction l as [|a l IHl] ; simpl ; [easy|].
     intros.
     apply IHl.
     unfold F.
@@ -993,7 +994,7 @@ Section MaxVar.
       (acc <= acc' ->
        fold_left F l acc <= fold_left F l acc')%positive.
   Proof.
-    induction l ; simpl ; [easy|].
+    intros l; induction l as [|a l IHl]; simpl ; [easy|].
     intros.
     apply IHl.
     unfold F.
@@ -1006,13 +1007,13 @@ Section MaxVar.
   Lemma max_var_nformulae_correct_aux : forall l p o v,
       In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive.
   Proof.
-  intros.
+  intros l p o v H H0.
   generalize 1%positive as acc.
   revert p o v H H0.
-  induction l.
+  induction l as [|a l IHl].
   - simpl. tauto.
   - simpl.
-    intros.
+    intros p o v H H0 ?.
     destruct H ; subst.
     + unfold F at 2.
       simpl.
@@ -1128,14 +1129,14 @@ Require Import Wf_nat.
 
 Lemma in_bdepth : forall l a b  y, In y l ->  ltof ZArithProof bdepth y (EnumProof a b  l).
 Proof.
-  induction l.
+  intros l; induction l as [|a l IHl].
   (* nil *)
   simpl.
   tauto.
   (* cons *)
   simpl.
-  intros.
-  destruct H.
+  intros a0 b y H.
+  destruct H as [H|H].
   subst.
   unfold ltof.
   simpl.
@@ -1180,8 +1181,8 @@ Lemma eval_Psatz_sound : forall env w l f',
   make_conj (eval_nformula env) l ->
   eval_Psatz l w  = Some f' ->  eval_nformula env f'.
 Proof.
-  intros.
-  apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto.
+  intros env w l f' H H0.
+  apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto.
   apply make_conj_in ; auto.
 Qed.
 
@@ -1193,7 +1194,7 @@ Proof.
   unfold nformula_of_cutting_plane.
   unfold eval_nformula. unfold RingMicromega.eval_nformula.
   unfold eval_op1.
-  intros.
+  intros env e e' c H H0.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
   simpl.
   (**)
@@ -1201,10 +1202,10 @@ Proof.
   revert H0.
   case_eq (Zgcd_pol e) ; intros g c0.
   generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0).
-  intros.
+  intros H0 H1 H2.
   inv H2.
   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *.
-  apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt.
+  apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt.
   apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r.
   apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
   apply Z.le_ge.
@@ -1213,7 +1214,7 @@ Proof.
   rewrite <- H1.
   assumption.
   (* g <= 0 *)
-  intros. inv H2. auto with zarith.
+  intros H0 H1 H2. inv H2. auto with zarith.
 Qed.
 
 Lemma cutting_plane_sound : forall env f p,
@@ -1222,34 +1223,34 @@ Lemma cutting_plane_sound : forall env f p,
    eval_nformula env (nformula_of_cutting_plane p).
 Proof.
   unfold genCuttingPlane.
-  destruct f as [e op].
+  intros env f; destruct f as [e op].
   destruct op.
   (* Equal *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (Zgcd_pol e) ; intros g c.
   case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|].
   case_eq (makeCuttingPlane e).
-  intros.
+  intros ? ? H H0 H1 H2 H3.
   inv H3.
   unfold makeCuttingPlane in H.
   rewrite H1 in H.
   revert H.
   change (eval_pol env e = 0) in H2.
   case_eq (Z.gtb g 0).
-  intros.
-  rewrite <- Zgt_is_gt_bool in H.  
+  intros H H3.
+  rewrite <- Zgt_is_gt_bool in H.
   rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2. 2: auto using Z.gt_lt.
-  unfold nformula_of_cutting_plane.  
+  unfold nformula_of_cutting_plane.
   change (eval_pol env (padd e' (Pc z)) = 0).
   inv H3.
   rewrite eval_pol_add.
   set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x.
   simpl.
   rewrite andb_false_iff in H0.
-  destruct H0.
+  destruct H0 as [H0|H0].
   rewrite Zgt_is_gt_bool in H ; congruence.
   rewrite andb_false_iff in H0.
-  destruct H0.
+  destruct H0 as [H0|H0].
   rewrite negb_false_iff in H0.
   apply Zeq_bool_eq in H0.
   subst. simpl.
@@ -1259,13 +1260,13 @@ Proof.
   apply Zeq_bool_eq in H0.
   assert (HH := Zgcd_is_gcd g c).
   rewrite H0 in HH.
-  inv HH.
+  destruct HH as [H3 H4 ?].
   apply Zdivide_opp_r in H4.
   rewrite Zdivide_ceiling ; auto.
   apply Z.sub_move_0_r.
   apply Z.div_unique_exact. now intros ->.
   now rewrite Z.add_move_0_r in H2.
-  intros.
+  intros H H3.
   unfold nformula_of_cutting_plane.
   inv H3.
   change (eval_pol env (padd e' (Pc 0)) = 0).
@@ -1273,7 +1274,7 @@ Proof.
   simpl.
   now rewrite Z.add_0_r.
   (* NonEqual *)
-  intros.
+  intros ? H H0.
   inv H0.
   unfold eval_nformula in *.
   unfold RingMicromega.eval_nformula in *.
@@ -1282,20 +1283,20 @@ Proof.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
   simpl. now rewrite Z.add_0_r.
   (* Strict *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (makeCuttingPlane (PsubC Z.sub e 1)).
-  intros.
+  intros ? ? H H0 H1.
   inv H1.
-  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
+  apply (makeCuttingPlane_ns_sound env) with (2:= H).
   simpl in *.
   rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
   now apply Z.lt_le_pred.
   (* NonStrict *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (makeCuttingPlane e).
-  intros.
+  intros ? ? H H0 H1.
   inv H1.
-  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
+  apply (makeCuttingPlane_ns_sound env) with (2:= H).
   assumption.
 Qed.
 
@@ -1304,12 +1305,15 @@ Lemma  genCuttingPlaneNone : forall env f,
   eval_nformula env f -> False.
 Proof.
   unfold genCuttingPlane.
-  destruct f.
+  intros env f; destruct f as [p o].
   destruct o.
   case_eq (Zgcd_pol p) ; intros g c.
   case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))).
-  intros.
+  intros H H0 H1 H2.
   flatten_bool.
+  match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end.
+  match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end.
+  match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end.
   rewrite negb_true_iff in H5.
   apply Zeq_bool_neq in H5.
   rewrite <- Zgt_is_gt_bool in H3.
@@ -1359,7 +1363,7 @@ Lemma agree_env_subset : forall v1 v2 env env',
     agree_env v2 env env'.
 Proof.
   unfold agree_env.
-  intros.
+  intros v1 v2 env env' H ? ? ?.
   apply H.
   eapply Pos.le_trans ; eauto.
 Qed.
@@ -1369,7 +1373,7 @@ Lemma agree_env_jump : forall fr j env env',
     agree_env (fr + j) env env' ->
     agree_env fr (Env.jump j env) (Env.jump j env').
 Proof.
-  intros.
+  intros fr j env env' H.
   unfold agree_env ; intro.
   intros.
   unfold Env.jump.
@@ -1382,7 +1386,7 @@ Lemma agree_env_tail : forall fr env env',
     agree_env (Pos.succ fr) env env' ->
     agree_env fr (Env.tail env) (Env.tail env').
 Proof.
-  intros.
+  intros fr env env' H.
   unfold Env.tail.
   apply agree_env_jump.
   rewrite <- Pos.add_1_r in H.
@@ -1393,7 +1397,7 @@ Qed.
 Lemma max_var_acc : forall p i j,
     (max_var (i + j) p = max_var i p + j)%positive.
 Proof.
-  induction p; simpl.
+  intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl.
   - reflexivity.
   - intros.
     rewrite ! IHp.
@@ -1415,27 +1419,27 @@ Lemma agree_env_eval_nformula :
          (AGREE : agree_env (max_var xH (fst e))  env env'),
     eval_nformula env e  <->  eval_nformula env' e.
 Proof.
-  destruct e.
-  simpl; intros.
+  intros env env' e; destruct e as [p o].
+  simpl; intros AGREE.
   assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p)
           =
-          (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)).
+          (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H.
   {
     revert env env' AGREE.
     generalize xH.
-    induction p ; simpl.
+    induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl.
     - reflexivity.
-    - intros.
-      apply IHp with (p := p1%positive).
+    - intros p1 **.
+      apply (IHp p1).
       apply agree_env_jump.
       eapply agree_env_subset; eauto.
       rewrite (Pos.add_comm p).
       rewrite max_var_acc.
       apply Pos.le_refl.
-    - intros.
+    - intros p ? ? AGREE.
       f_equal.
       f_equal.
-      { apply IHp1 with (p:= p).
+      { apply (IHp1 p).
         eapply agree_env_subset; eauto.
         apply Pos.le_max_l.
       }
@@ -1446,7 +1450,7 @@ Proof.
         apply Pos.le_1_l.
       }
       {
-        apply IHp2 with (p := p).
+        apply (IHp2 p).
         apply agree_env_tail.
         eapply agree_env_subset; eauto.
         rewrite !Pplus_one_succ_r.
@@ -1463,11 +1467,11 @@ Lemma agree_env_eval_nformulae :
          make_conj (eval_nformula env) l <->
          make_conj (eval_nformula env') l.
 Proof.
-  induction l.
+  intros env env' l; induction l as [|a l IHl].
   - simpl. tauto.
   - intros.
     rewrite ! make_conj_cons.
-    assert (eval_nformula env a <-> eval_nformula env' a).
+    assert (eval_nformula env a <-> eval_nformula env' a) as H.
     {
       apply agree_env_eval_nformula.
       eapply agree_env_subset ; eauto.
@@ -1491,7 +1495,7 @@ Qed.
 Lemma eq_true_iff_eq :
   forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2.
 Proof.
-  destruct b1,b2 ; intuition congruence.
+  intros b1 b2; destruct b1,b2 ; intuition congruence.
 Qed.
 
 Ltac pos_tac :=
@@ -1520,7 +1524,7 @@ Qed.
 Lemma ZChecker_sound : forall w l,
     ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
 Proof.
-  induction w    using (well_founded_ind (well_founded_ltof _ bdepth)).
+  intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)).
   destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf].
   - (* DoneProof *)
   simpl. discriminate.
@@ -1529,12 +1533,12 @@ Proof.
   intros l. case_eq (eval_Psatz l w) ; [| discriminate].
   intros f Hf.
   case_eq (Zunsat f).
-  intros.
+  intros H0 ? ?.
   apply (checker_nf_sound Zsor ZSORaddon l w).
   unfold check_normalised_formulas.  unfold eval_Psatz in Hf. rewrite Hf.
   unfold Zunsat in H0. assumption.
-  intros.
-  assert (make_impl  (eval_nformula env) (f::l) False).
+  intros H0 H1 env.
+  assert (make_impl  (eval_nformula env) (f::l) False) as H2.
    apply H with (2:= H1).
    unfold ltof.
    simpl.
@@ -1553,8 +1557,8 @@ Proof.
   case_eq (eval_Psatz l w) ; [ | discriminate].
   intros f' Hlc.
   case_eq (genCuttingPlane f').
-  intros.
-  assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
+  intros p H0 H1 env.
+  assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2.
    eapply (H pf)  ; auto.
    unfold ltof.
    simpl.
@@ -1565,13 +1569,13 @@ Proof.
   intro.
   apply H2.
   split ; auto.
-  apply eval_Psatz_sound with (env:=env) in Hlc.
+  apply (eval_Psatz_sound env) in Hlc.
   apply cutting_plane_sound with (1:= Hlc) (2:= H0).
   auto.
   (* genCuttingPlane = None *)
-  intros.
+  intros H0 H1 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H2.
   apply eval_Psatz_sound with (2:= Hlc) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
   - (* SplitProof *)
@@ -1581,18 +1585,20 @@ Proof.
     case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate].
     intros cp1 GCP1 cp2 GCP2 ZC1 env.
     flatten_bool.
+    match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end.
+    match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end.
     destruct (eval_nformula_split env p).
-    + apply H with (env:=env) in H0.
+    + apply (fun H' ck => H _ H' _ ck env) in H0.
       rewrite <- make_conj_impl in *.
       intro ; apply H0.
       rewrite make_conj_cons. split; auto.
-      apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto.
+      apply (cutting_plane_sound _ (p,NonStrict)) ; auto.
       apply ltof_bdepth_split_l.
-    + apply H with (env:=env) in H1.
+    + apply (fun H' ck => H _ H' _ ck env) in H1.
       rewrite <- make_conj_impl in *.
       intro ; apply H1.
       rewrite make_conj_cons. split; auto.
-      apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto.
+      apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto.
       apply ltof_bdepth_split_r.
   - (* EnumProof *)
   intros l.
@@ -1601,22 +1607,22 @@ Proof.
   case_eq (eval_Psatz l w2) ; [  | discriminate].
   intros f1 Hf1 f2 Hf2.
   case_eq (genCuttingPlane f2).
-  destruct p as [ [p1 z1] op1].
+  intros p; destruct p as [ [p1 z1] op1].
   case_eq (genCuttingPlane f1).
-  destruct p as [ [p2 z2] op2].
+  intros p; destruct p as [ [p2 z2] op2].
   case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)).
   intros Hcond.
   flatten_bool.
-  rename H1 into HZ0.
-  rename H2 into Hop1.
-  rename H3 into Hop2.
+  match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end.
+  match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end.
+  match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end.
   intros HCutL HCutR Hfix env.
   (* get the bounds of the enum *)
   rewrite <- make_conj_impl.
-  intro.
-  assert (-z1 <= eval_pol env p1 <= z2).
+  intro H0.
+  assert (-z1 <= eval_pol env p1 <= z2) as H1.
    split.
-   apply  eval_Psatz_sound with (env:=env) in Hf2 ; auto.
+   apply  (eval_Psatz_sound env) in Hf2 ; auto.
    apply cutting_plane_sound with (1:= Hf2) in HCutR.
    unfold nformula_of_cutting_plane in HCutR.
    unfold eval_nformula in HCutR.
@@ -1628,10 +1634,10 @@ Proof.
      rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity.
      now apply Z.le_sub_le_add_r in HCutR.
    (**)
-   apply is_pol_Z0_eval_pol with (env := env) in HZ0.
+   apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0.
    rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0.
    rewrite HZ0.
-   apply  eval_Psatz_sound with (env:=env) in Hf1 ; auto.
+   apply  (eval_Psatz_sound env) in Hf1 ; auto.
    apply cutting_plane_sound with (1:= Hf1) in HCutL.
    unfold nformula_of_cutting_plane in HCutL.
    unfold eval_nformula in HCutL.
@@ -1647,7 +1653,7 @@ Proof.
   match goal with
     | |- context[?F pf (-z1) z2 = true] => set (FF := F)
   end.
-  intros.
+  intros Hfix.
   assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
     (In pr pf /\
       ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
@@ -1655,16 +1661,18 @@ Proof.
   revert Hfix.
   generalize (-z1). clear z1. intro z1.
   revert z1 z2.
-  induction pf;simpl ;intros.
+  induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **.
   revert Hfix.
   now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x.
   flatten_bool.
+  match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end.
+  match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end.
   destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ].
   2: exists a; auto.
   rewrite <- Z.le_succ_l in LT.
   assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition.
   elim IHpf with (2:=H2) (3:= LE).
-  intros.
+  intros x0 ?.
   exists x0 ; split;tauto.
   intros until 1. 
   apply H ; auto. 
@@ -1676,7 +1684,7 @@ Proof.
   apply Z.add_le_mono_r. assumption.
   (*/asser *)
   destruct (HH _ H1) as [pr [Hin Hcheker]].
-  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
+  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2.
    eapply (H pr)  ;auto.
    apply in_bdepth ; auto.
   rewrite <- make_conj_impl in H2.
@@ -1690,15 +1698,15 @@ Proof.
   unfold eval_pol. ring.
   discriminate.
   (* No cutting plane *)
-  intros.
+  intros H0 H1 H2 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H3.
   apply eval_Psatz_sound with (2:= Hf1) in H3.
   apply genCuttingPlaneNone with (2:= H3) ; auto.
   (* No Cutting plane (bis) *)
-  intros.
+  intros H0 H1 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H2.
   apply eval_Psatz_sound with (2:= Hf2) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
 - intros l.
@@ -1708,15 +1716,15 @@ Proof.
   set (z1 := (Pos.succ fr)) in *.
   set (t1 := (Pos.succ z1)) in *.
   destruct (x <=? fr)%positive eqn:LE ; [|congruence].
-  intros.
+  intros H0 env.
   set (env':= fun v => if Pos.eqb v z1
                        then if Z.leb (env x) 0 then 0 else env x
                        else if Pos.eqb v t1
                             then if Z.leb (env x) 0 then -(env x) else 0
                             else env v).
-  apply H with (env:=env') in H0.
+  apply (fun H' ck => H _ H' _ ck env') in H0.
   + rewrite <- make_conj_impl in *.
-    intro.
+    intro H1.
     rewrite !make_conj_cons in H0.
     apply H0 ; repeat split.
     *
@@ -1729,17 +1737,17 @@ Proof.
       destruct (env x <=? 0); ring.
       { unfold t1.
         pos_tac; normZ.
-        lia (Hyp H2).
+        lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)).
       }
       {
         unfold t1, z1.
         pos_tac; normZ.
-        lia (Add (Hyp LE) (Hyp H3)).
+        lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))).
       }
       {
         unfold z1.
         pos_tac; normZ.
-        lia (Add (Hyp LE) (Hyp H3)).
+        lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))).
       }
     *
       apply eval_nformula_bound_var.
@@ -1749,7 +1757,7 @@ Proof.
       compute. congruence.
       rewrite Z.leb_gt in EQ.
       normZ.
-      lia (Add (Hyp EQ) (Hyp H2)).
+      lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))).
     *
       apply eval_nformula_bound_var.
       unfold env'.
@@ -1758,15 +1766,15 @@ Proof.
       destruct (env x <=? 0) eqn:EQ.
       rewrite Z.leb_le in EQ.
       normZ.
-      lia (Add (Hyp EQ) (Hyp H2)).
+      lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))).
       compute; congruence.
       unfold t1.
       clear.
       pos_tac; normZ.
-      lia (Hyp H).
+      lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)).
     *
-      rewrite agree_env_eval_nformulae with (env':= env') in H1;auto.
-      unfold agree_env; intros.
+      rewrite (agree_env_eval_nformulae _ env') in H1;auto.
+      unfold agree_env; intros x0 H2.
       unfold env'.
       replace (x0 =? z1)%positive with false.
       replace (x0 =? t1)%positive with false.
@@ -1776,13 +1784,13 @@ Proof.
         unfold fr in *.
         apply Pos2Z.pos_le_pos in H2.
         pos_tac; normZ.
-        lia (Add (Hyp H2) (Hyp H4)).
+        lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))).
       }
       {
         unfold z1, fr in *.
         apply Pos2Z.pos_le_pos in H2.
         pos_tac; normZ.
-        lia (Add (Hyp H2) (Hyp H4)).
+        lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))).
       }
   + unfold ltof.
     simpl.
@@ -1796,27 +1804,27 @@ Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env,
 Proof.
   intros f w.
   unfold ZTautoChecker.
-  apply tauto_checker_sound with (eval' := eval_nformula).
+  apply (tauto_checker_sound _ _ _ _ eval_nformula).
   - apply Zeval_nformula_dec.
-  - intros until env.
+  - intros t ? env.
   unfold eval_nformula. unfold RingMicromega.eval_nformula.
   destruct t.
   apply (check_inconsistent_sound Zsor ZSORaddon) ; auto.
-  - unfold Zdeduce. intros. revert H.
+  - unfold Zdeduce. intros ? ? ? H **. revert H.
      apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto.
   -
-    intros.
+    intros ? ? ? ? H.
     rewrite normalise_correct  in H.
     rewrite Zeval_formula_compat; auto.
   -
-    intros.
+    intros ? ? ? ? H.
     rewrite negate_correct in H ; auto.
     rewrite Tauto.hold_eNOT.
     rewrite Zeval_formula_compat; auto.
   - intros t w0.
     unfold eval_tt.
-    intros.
-    rewrite make_impl_map with (eval := eval_nformula env).
+    intros H env.
+    rewrite (make_impl_map (eval_nformula env)).
     eapply ZChecker_sound; eauto.
     tauto.
 Qed.