2 files changed, 7 insertions, 7 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 3cfa55bef..93ae858d8 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -475,7 +475,7 @@ Module Make (W0:CyclicType) <: NType.
     DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
   fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).
 
- Let div_gtnm n m wx wy :=
+ Definition div_gtnm n m wx wy :=
     let mn := Max.max n m in
     let d := diff n m in
     let op := make_op mn in
@@ -522,7 +522,7 @@ Module Make (W0:CyclicType) <: NType.
   case (ZnZ.spec_to_Z y); auto.
  Qed.
 
- Let spec_divn1 n :=
+ Definition spec_divn1 n :=
    DoubleDivn1.spec_double_divn1
     (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
     ZnZ.WW ZnZ.head0
@@ -643,7 +643,7 @@ Module Make (W0:CyclicType) <: NType.
     DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
   fun m x y => reduce n (dmodn1 (S m) x y).
 
- Let mod_gtnm n m wx wy :=
+ Definition mod_gtnm n m wx wy :=
     let mn := Max.max n m in
     let d := diff n m in
     let op := make_op mn in
@@ -671,7 +671,7 @@ Module Make (W0:CyclicType) <: NType.
   reflexivity.
  Qed.
 
- Let spec_modn1 n :=
+ Definition spec_modn1 n :=
    DoubleDivn1.spec_double_modn1
     (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
     ZnZ.WW ZnZ.head0
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 278cc8bf7..b941ed48f 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -234,7 +234,7 @@ pr
   | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1)
   end.
 
- Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
+ Definition eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m).
 
  Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x,
    nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x).
@@ -533,7 +533,7 @@ pr "
 for i = 0 to size-1 do
 let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in
 pr
-" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
+" Definition mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in
   match m return word w%i (S m) -> t with
     | %s as p => mk_t_w %i (S p)
     | p => mk_t (%i+p)
@@ -542,7 +542,7 @@ pr
 done;
 
 pr
-" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
+" Definition mk_t_w' n : forall m, word (dom_t n) (S m) -> t :=
   match n return (forall m, word (dom_t n) (S m) -> t) with";
 for i = 0 to size-1 do pr "    | %i => mk_t_%iw" i i done;
 pr