2 files changed, 13 insertions, 13 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 215b8bd5..d160f5f1 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -19,13 +19,13 @@ Local Open Scope list_scope.
 
 Ltac isInt31cst_lst l :=
  match l with
- | nil => constr:true
+ | nil => constr:(true)
  | ?t::?l => match t with
                | D1 => isInt31cst_lst l
                | D0 => isInt31cst_lst l
-               | _ => constr:false
+               | _ => constr:(false)
              end
- | _ => constr:false
+ | _ => constr:(false)
  end.
 
 Ltac isInt31cst t :=
@@ -38,17 +38,17 @@ Ltac isInt31cst t :=
       ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
       ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
     in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
+ | Int31.On => constr:(true)
+ | Int31.In => constr:(true)
+ | Int31.Tn => constr:(true)
+ | Int31.Twon => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac Int31cst t :=
  match isInt31cst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** The generic ring structure inferred from the Cyclic structure *)
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index c115a831..04fc5a8d 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -369,7 +369,7 @@ Section ZModulo.
  assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H; clear H; intros.
+ destruct 1; injection H as ? ?.
  rewrite H0.
  assert ([|l|] = l).
   apply Zmod_small; auto.
@@ -411,7 +411,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod [|a|] [|b|] H0).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1; clear H1; intros.
+ injection H1 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
@@ -522,7 +522,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod a [|b|] H3).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4; clear H4; intros.
+ injection H4 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.