aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Peano_dec.v6
-rw-r--r--theories/FSets/FMapAVL.v18
-rw-r--r--theories/FSets/FMapFullAVL.v8
-rw-r--r--theories/FSets/FMapPositive.v6
-rw-r--r--theories/FSets/FSetBridge.v8
-rw-r--r--theories/FSets/FSetInterface.v2
-rw-r--r--theories/Init/Specif.v8
-rw-r--r--theories/Logic/Eqdep_dec.v2
-rw-r--r--theories/NArith/Ndigits.v6
-rw-r--r--theories/Reals/RiemannInt_SF.v2
-rw-r--r--theories/Vectors/Fin.v56
-rw-r--r--theories/Vectors/VectorDef.v16
-rw-r--r--theories/ZArith/Zsqrt_compat.v12
13 files changed, 75 insertions, 75 deletions
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index e0bed0d37..9b8ebfe55 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -38,15 +38,15 @@ Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
Proof.
fix 3.
refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
- with le_n => _ |le_S i H => _ end).
+ with le_n _ => _ |le_S _ i H => _ end).
refine (fun hh => match hh as h' in _ <= k return forall eq: m = k,
le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
- |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl).
+ |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl).
rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
subst m. destruct (Lt.lt_irrefl j H').
refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
- with |le_n => _ |le_S j H2 => fun H' => _ end H).
+ with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H).
destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
f_equal. apply le_unique.
Qed.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f42f1e9e0..5d34a4bf5 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -342,7 +342,7 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
match m with
- | Leaf => Leaf _
+ | Leaf _ => Leaf _
| Node l x d r h => Node (map f l) x (f d) (map f r) h
end.
@@ -350,7 +350,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
match m with
- | Leaf => Leaf _
+ | Leaf _ => Leaf _
| Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
end.
@@ -359,7 +359,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
: t elt' :=
match m with
- | Leaf => Leaf _
+ | Leaf _ => Leaf _
| Node l x d r h =>
match f x d with
| Some d' => join (map_option f l) x d' (map_option f r)
@@ -389,8 +389,8 @@ Variable mapr : t elt' -> t elt''.
Fixpoint map2_opt m1 m2 :=
match m1, m2 with
- | Leaf, _ => mapr m2
- | _, Leaf => mapl m1
+ | Leaf _, _ => mapr m2
+ | _, Leaf _ => mapl m1
| Node l1 x1 d1 r1 h1, _ =>
let (l2',o2,r2') := split x1 m2 in
match f x1 d1 o2 with
@@ -1424,7 +1424,7 @@ Qed.
i.e. the list of elements actually compared *)
Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
- | End => nil
+ | End _ => nil
| More x e t r => (x,e) :: elements t ++ flatten_e r
end.
@@ -2016,7 +2016,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
match e2 with
- | R.End => Gt
+ | R.End _ => Gt
| R.More x2 d2 r2 e2 =>
match X.compare x1 x2 with
| EQ _ => match D.compare d1 d2 with
@@ -2033,7 +2033,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
match s1 with
- | R.Leaf => cont e2
+ | R.Leaf _ => cont e2
| R.Node l1 x1 d1 r1 _ =>
compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
end.
@@ -2041,7 +2041,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
(** Initial continuation *)
Definition compare_end (e2:R.enumeration D.t) :=
- match e2 with R.End => Eq | _ => Lt end.
+ match e2 with R.End _ => Eq | _ => Lt end.
(** The complete comparison *)
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index e1c603514..59b778369 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
match e with
- | Raw.End => 0%nat
+ | Raw.End _ => 0%nat
| Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
end.
@@ -677,9 +677,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
{ measure cardinal_e_2 ee } : comparison :=
match ee with
- | (Raw.End, Raw.End) => Eq
- | (Raw.End, Raw.More _ _ _ _) => Lt
- | (Raw.More _ _ _ _, Raw.End) => Gt
+ | (Raw.End _, Raw.End _) => Eq
+ | (Raw.End _, Raw.More _ _ _ _) => Lt
+ | (Raw.More _ _ _ _, Raw.End _) => Gt
| (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
match X.compare x1 x2 with
| EQ _ => match D.compare d1 d2 with
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index d562245d8..5e968d4d3 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -902,7 +902,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
match m with
- | Leaf => v
+ | Leaf _ => v
| Node l (Some x) r =>
xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
| Node l None r =>
@@ -940,8 +940,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool :=
match m1, m2 with
- | Leaf, _ => is_empty m2
- | _, Leaf => is_empty m1
+ | Leaf _, _ => is_empty m2
+ | _, Leaf _ => is_empty m1
| Node l1 o1 r1, Node l2 o2 r2 =>
(match o1, o2 with
| None, None => true
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 1ac544e1f..6aebcf501 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -284,7 +284,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
Lemma choose_equal : forall s s', Equal s s' ->
match choose s, choose s' with
- | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+ | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
| inright _, inright _ => True
| _, _ => False
end.
@@ -423,7 +423,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Definition choose (s : t) : option elt :=
match choose s with
- | inleft (exist x _) => Some x
+ | inleft (exist _ x _) => Some x
| inright _ => None
end.
@@ -472,7 +472,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Definition min_elt (s : t) : option elt :=
match min_elt s with
- | inleft (exist x _) => Some x
+ | inleft (exist _ x _) => Some x
| inright _ => None
end.
@@ -500,7 +500,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Definition max_elt (s : t) : option elt :=
match max_elt s with
- | inleft (exist x _) => Some x
+ | inleft (exist _ x _) => Some x
| inright _ => None
end.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index a03611193..c791f49a6 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -497,7 +497,7 @@ Module Type Sdep.
in the dependent version of [choose], so we leave it separate. *)
Parameter choose_equal : forall s s', Equal s s' ->
match choose s, choose s' with
- | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+ | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
| inright _, inright _ => True
| _, _ => False
end.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1610f0a1..6adc1c369 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -72,12 +72,12 @@ Section Subset_projections.
Variable P : A -> Prop.
Definition proj1_sig (e:sig P) := match e with
- | exist a b => a
+ | exist _ a b => a
end.
Definition proj2_sig (e:sig P) :=
match e return P (proj1_sig e) with
- | exist a b => b
+ | exist _ a b => b
end.
End Subset_projections.
@@ -96,11 +96,11 @@ Section Projections.
Variable P : A -> Type.
Definition projT1 (x:sigT P) : A := match x with
- | existT a _ => a
+ | existT _ a _ => a
end.
Definition projT2 (x:sigT P) : P (projT1 x) :=
match x return P (projT1 x) with
- | existT _ h => h
+ | existT _ _ h => h
end.
End Projections.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index ea5b16517..9bde2d641 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -101,7 +101,7 @@ Section EqdepDec.
Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
match exP with
- | ex_intro x' prf =>
+ | ex_intro _ x' prf =>
match eq_dec x' x with
| or_introl eqprf => eq_ind x' P prf x eqprf
| _ => def
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index b50adaab8..662c50abf 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -512,9 +512,9 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
match bv with
- | Vector.nil => N0
- | Vector.cons false n bv => N.double (Bv2N n bv)
- | Vector.cons true n bv => N.succ_double (Bv2N n bv)
+ | Vector.nil _ => N0
+ | Vector.cons _ false n bv => N.double (Bv2N n bv)
+ | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
end.
Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d523a1f44..9de60bb5d 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -144,7 +144,7 @@ Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f).
Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
match projT2 (pre f) with
- | existT a b => a
+ | existT _ a b => a
end.
Fixpoint Int_SF (l k:Rlist) : R :=
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index ae33e6318..b6ec6307c 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -23,14 +23,14 @@ Inductive t : nat -> Set :=
Section SCHEMES.
Definition case0 P (p: t 0): P p :=
- match p with | F1 _ | FS _ _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
+ match p with | F1 | FS _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
Definition caseS (P: forall {n}, t (S n) -> Type)
(P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
{n} (p: t (S n)): P p :=
match p with
- |F1 k => P1 k
- |FS k pp => PS pp
+ |@F1 k => P1 k
+ |FS pp => PS pp
end.
Definition rectS (P: forall {n}, t (S n) -> Type)
@@ -38,9 +38,9 @@ Definition rectS (P: forall {n}, t (S n) -> Type)
forall {n} (p: t (S n)), P p :=
fix rectS_fix {n} (p: t (S n)): P p:=
match p with
- |F1 k => P1 k
- |FS 0 pp => case0 (fun f => P (FS f)) pp
- |FS (S k) pp => PS pp (rectS_fix pp)
+ |@F1 k => P1 k
+ |@FS 0 pp => case0 (fun f => P (FS f)) pp
+ |@FS (S k) pp => PS pp (rectS_fix pp)
end.
Definition rect2 (P: forall {n} (a b: t n), Type)
@@ -51,14 +51,14 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
forall {n} (a b: t n), P a b :=
fix rect2_fix {n} (a: t n): forall (b: t n), P a b :=
match a with
- |F1 m => fun (b: t (S m)) => match b as b' in t (S n')
+ |@F1 m => fun (b: t (S m)) => match b as b' in t (S n')
return P F1 b' with
- |F1 m' => H0 m'
- |FS m' b' => H1 b'
+ |@F1 m' => H0 m'
+ |FS b' => H1 b'
end
- |FS m a' => fun (b: t (S m)) => match b with
- |F1 m' => fun aa: t m' => H2 aa
- |FS m' b' => fun aa: t m' => HS aa b' (rect2_fix aa b')
+ |@FS m a' => fun (b: t (S m)) => match b with
+ |@F1 m' => fun aa: t m' => H2 aa
+ |FS b' => fun aa => HS aa b' (rect2_fix aa b')
end a'
end.
End SCHEMES.
@@ -66,15 +66,15 @@ End SCHEMES.
Definition FS_inj {n} (x y: t n) (eq: FS x = FS y): x = y :=
match eq in _ = a return
match a as a' in t m return match m with |0 => Prop |S n' => t n' -> Prop end
- with @F1 _ => fun _ => True |@FS _ y => fun x' => x' = y end x with
+ with F1 => fun _ => True |FS y => fun x' => x' = y end x with
eq_refl => eq_refl
end.
(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
match n with
- |F1 j => exist _ 0 (Lt.lt_0_Sn j)
- |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
+ |@F1 j => exist _ 0 (Lt.lt_0_Sn j)
+ |FS p => match to_nat p with |exist _ i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
end.
(** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of
@@ -86,7 +86,7 @@ Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
|0 => inleft _ (F1)
|S p' => match of_nat p' n' with
|inleft f => inleft _ (FS f)
- |inright arg => inright _ (match arg with |ex_intro m e =>
+ |inright arg => inright _ (match arg with |ex_intro _ m e =>
ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
end
end
@@ -118,15 +118,15 @@ Fixpoint weak {m}{n} p (f : t m -> t n) :
match p as p' return t (p' + m) -> t (p' + n) with
|0 => f
|S p' => fun x => match x with
- |F1 n' => fun eq : n' = p' + m => F1
- |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
+ |@F1 n' => fun eq : n' = p' + m => F1
+ |@FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
end (eq_refl _)
end.
(** The p{^ th} element of [fin m] viewed as the p{^ th} element of
[fin (m + n)] *)
Fixpoint L {m} n (p : t m) : t (m + n) :=
- match p with |F1 _ => F1 |FS _ p' => FS (L n p') end.
+ match p with |F1 => F1 |FS p' => FS (L n p') end.
Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
Proof.
@@ -144,8 +144,8 @@ induction n.
exact p.
exact ((fix LS k (p: t k) :=
match p with
- |F1 k' => @F1 (S k')
- |FS _ p' => FS (LS _ p')
+ |@F1 k' => @F1 (S k')
+ |FS p' => FS (LS _ p')
end) _ IHn).
Defined.
@@ -163,8 +163,8 @@ Qed.
Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
match o with
- |F1 m' => L (m' * n) p
- |FS m' o' => R n (depair o' p)
+ |@F1 m' => L (m' * n) p
+ |FS o' => R n (depair o' p)
end.
Lemma depair_sanity {m n} (o : t m) (p : t n) :
@@ -181,9 +181,9 @@ Qed.
Fixpoint eqb {m n} (p : t m) (q : t n) :=
match p, q with
| @F1 m', @F1 n' => EqNat.beq_nat m' n'
-| @FS _ _, @F1 _ => false
-| @F1 _, @FS _ _ => false
-| @FS _ p', @FS _ q' => eqb p' q'
+| FS _, F1 => false
+| F1, FS _ => false
+| FS p', FS q' => eqb p' q'
end.
Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.
@@ -219,11 +219,11 @@ Definition cast: forall {m} (v: t m) {n}, m = n -> t n.
Proof.
refine (fix cast {m} (v: t m) {struct v} :=
match v in t m' return forall n, m' = n -> t n with
- |@F1 _ => fun n => match n with
+ |F1 => fun n => match n with
| 0 => fun H => False_rect _ _
| S n' => fun H => F1
end
- |@FS _ f => fun n => match n with
+ |FS f => fun n => match n with
| 0 => fun H => False_rect _ _
| S n' => fun H => FS (cast f n' (f_equal pred H))
end
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 30a8c5699..64c69ba24 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,12 +40,12 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
(rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
fix rectS_fix {n} (v: t A (S n)) : P v :=
match v with
- |cons a 0 v =>
+ |@cons _ a 0 v =>
match v with
- |nil => bas a
+ |nil _ => bas a
|_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end
- |cons a (S nn') v => rect a v (rectS_fix v)
+ |@cons _ a (S nn') v => rect a v (rectS_fix v)
|_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end.
@@ -109,8 +109,8 @@ ocaml function. *)
Definition nth {A} :=
fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
match p in Fin.t m' return t A m' -> A with
- |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v
- |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
+ |Fin.F1 => fun v => caseS (fun n v' => A) (fun h n t => h) v
+ |Fin.FS p' => fun v => (caseS (fun n v' => Fin.t n -> A)
(fun h n t p0 => nth_fix t p0) v) p'
end v'.
@@ -121,8 +121,8 @@ Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
(** Put [a] at the p{^ th} place of [v] *)
Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
match p with
- |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
- |Fin.FS k p' => fun v' =>
+ |@Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
+ |Fin.FS p' => fun v' =>
(caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) v') p'
end v.
@@ -251,7 +251,7 @@ match v in t _ n0 return t C n0 -> A with
|[] => a
|_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end
- |cons vh vn vt => fun w => match w with
+ |@cons _ vh vn vt => fun w => match w with
|wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt
|_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
end vt
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index a6c832412..9e8d9372c 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -53,7 +53,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
| xI xH => c_sqrt 3 1 2 _ _
| xO (xO p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r') with
| left Hle =>
c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1)
@@ -63,7 +63,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xO (xI p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with
| left Hle =>
c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1)
@@ -74,7 +74,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xI (xO p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with
| left Hle =>
c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1)
@@ -85,7 +85,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
end
| xI (xI p') =>
match sqrtrempos p' with
- | c_sqrt s' r' Heq Hint =>
+ | c_sqrt _ s' r' Heq Hint =>
match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with
| left Hle =>
c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1)
@@ -114,7 +114,7 @@ Definition Zsqrt :
| Zpos p =>
fun h =>
match sqrtrempos p with
- | c_sqrt s r Heq Hint =>
+ | c_sqrt _ s r Heq Hint =>
existT
(fun s:Z =>
{r : Z |
@@ -150,7 +150,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
match x with
| Zpos p =>
match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with
- | existT s _ => s
+ | existT _ s _ => s
end
| Zneg p => 0
| Z0 => 0
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 16:12:22 +0000