Adapt the various "Let" with Qed

In sections: use #[clearbody] and Defined instead
At toplevel: use Local Lemma instead

BigN/BigN.v

@@ -177,7 +177,7 @@ Add Ring BigNr : BigNring
 Section TestRing.
 Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
 intros. ring_simplify. reflexivity.
-Qed.
+Defined.
 End TestRing.
 
 (** We benefit also from an "order" tactic *)
@@ -186,12 +186,12 @@ Ltac bigN_order := BigN.order.
 
 Section TestOrder.
 Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
-Proof. bigN_order. Qed.
+Proof. bigN_order. Defined.
 End TestOrder.
 
 (** We can use at least a bit of lia by translating to [Z]. *)
 
 Section TestLia.
 Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
-Proof. intros x y. BigN.zify. lia. Qed.
+Proof. intros x y. BigN.zify. lia. Defined.
 End TestLia.

BigN/NMake.v

@@ -247,7 +247,7 @@ Module Make (W0:CyclicType) <: NType.
   let compare0 := compare zero in
   fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
 
- Let spec_comparen_m:
+ Local Lemma spec_comparen_m:
   forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
    comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
  Proof.

BigN/gen/NMake_gen.ml

@@ -305,7 +305,7 @@ pr "
   do_size (destruct n; auto with *). apply wn_spec.
  Qed.
 
- Let make_op_WW : forall n x y,
+ Local Lemma make_op_WW : forall n x y,
    (ZnZ.to_Z (Ops:=make_op (S n)) (WW x y) =
     ZnZ.to_Z (Ops:=make_op n) x * base (ZnZ.digits (make_op n))
      + ZnZ.to_Z (Ops:=make_op n) y)%%Z.
@@ -601,7 +601,7 @@ pr
 
  (** Misc results about extensions *)
 
- Let spec_extend_WW : forall n x,
+ Local Lemma spec_extend_WW : forall n x,
   [Nn (S n) (WW W0 x)] = [Nn n x].
  Proof.
  intros n x.
@@ -611,23 +611,23 @@ pr
  solve_eval.
  Qed.
 
- Let spec_extend_tr: forall m n w,
+ Local Lemma spec_extend_tr: forall m n w,
  [Nn (m + n) (extend_tr w m)] = [Nn n w].
  Proof.
  induction m; auto.
  intros n x; simpl extend_tr.
  simpl plus; rewrite spec_extend_WW; auto.
  Qed.
 
- Let spec_cast_l: forall n m x1,
+ Local Lemma spec_cast_l: forall n m x1,
  [Nn n x1] =
  [Nn (Nat.max n m) (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))].
  Proof.
  intros n m x1; case (diff_r n m); simpl castm.
  rewrite spec_extend_tr; auto.
  Qed.
 
- Let spec_cast_r: forall n m x1,
+ Local Lemma spec_cast_r: forall n m x1,
  [Nn m x1] =
  [Nn (Nat.max n m) (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))].
  Proof.
@@ -661,11 +661,12 @@ done;
 pr
 "  Let fn n := f (SizePlus (S n)).
 
+  #[clearbody]
   Let Pf' :
    forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
   Proof.
   intros. subst. rewrite 2 spec_mk_t. apply Pf.
-  Qed.
+  Defined.
 ";
 
 let ext i j s =
@@ -753,23 +754,26 @@ pr
   Variable fnm: forall n m, word (dom_t Size) (S n) -> word (dom_t Size) (S m) -> res.
   Variable Pfnm: forall n m x y, P [Nn n x] [Nn m y] (fnm n m x y).
 
+  #[clearbody]
   Let Pf' :
    forall n x y u v, u = [mk_t n x] -> v = [mk_t n y] -> P u v (f n x y).
   Proof.
   intros. subst. rewrite 2 spec_mk_t. apply Pf.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let Pfd' : forall n m x y u v, u = [mk_t n x] -> v = eval n (S m) y ->
    P u v (fd n m x y).
   Proof.
   intros. subst. rewrite spec_mk_t. apply Pfd.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let Pfg' : forall n m x y u v, u = eval n (S m) x -> v = [mk_t n y] ->
    P u v (fg n m x y).
   Proof.
   intros. subst. rewrite spec_mk_t. apply Pfg.
-  Qed.
+  Defined.
 ";
 
 for i = 0 to size do

BigQ/BigQ.v

@@ -142,21 +142,24 @@ Add Field BigQfield : BigQfieldth
 
 Section TestField.
 
+#[clearbody]
 Let ex1 : forall x y z, (x+y)*z ==  (x*z)+(y*z).
   intros.
   ring.
-Qed.
+Defined.
 
+#[clearbody]
 Let ex8 : forall x, x ^ 2 == x*x.
   intro.
   ring.
-Qed.
+Defined.
 
+#[clearbody]
 Let ex10 : forall x y, y!=0 -> (x/y)*y == x.
 intros.
 field.
 auto.
-Qed.
+Defined.
 
 End TestField.
 
@@ -166,13 +169,13 @@ Ltac bigQ_order := BigQ.order.
 
 Section TestOrder.
 Let test : forall x y : bigQ, x<=y -> y<=x -> x==y.
-Proof. bigQ_order. Qed.
+Proof. bigQ_order. Defined.
 End TestOrder.
 
 (** We can also reason by switching to QArith thanks to tactic
     BigQ.qify. *)
 
 Section TestQify.
 Let test : forall x : bigQ, 0+x == 1*x.
-Proof. intro x. BigQ.qify. ring. Qed.
+Proof. intro x. BigQ.qify. ring. Defined.
 End TestQify.

BigZ/BigZ.v

@@ -181,14 +181,16 @@ Add Ring BigZr : BigZring
   div BigZdiv).
 
 Section TestRing.
+#[clearbody]
 Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
 Proof.
 intros. ring_simplify. reflexivity.
-Qed.
+Defined.
+#[clearbody]
 Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0.
 Proof.
 intros. ring_simplify. reflexivity.
-Qed.
+Defined.
 End TestRing.
 
 (** [BigZ] also benefits from an "order" tactic *)
@@ -197,12 +199,12 @@ Ltac bigZ_order := BigZ.order.
 
 Section TestOrder.
 Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
-Proof. bigZ_order. Qed.
+Proof. bigZ_order. Defined.
 End TestOrder.
 
 (** We can use at least a bit of lia by translating to [Z]. *)
 
 Section TestLia.
 Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
-Proof. intros x y. BigZ.zify. Lia.lia. Qed.
+Proof. intros x y. BigZ.zify. Lia.lia. Defined.
 End TestLia.