diff options
50 files changed, 348 insertions, 336 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 7f6f5672b..449979162 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -19,7 +19,7 @@ open Constrexpr_ops (*i*) -let oldfashion_patterns = ref (true) +let oldfashion_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index 792e2c3c2..c580ba75b 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -66,7 +66,7 @@ Require Import EnvRing. Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q := match e with | PEc c => c - | PEX j => env j + | PEX _ j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) @@ -78,7 +78,7 @@ Lemma Qeval_expr_simpl : forall env e, Qeval_expr env e = match e with | PEc c => c - | PEX j => env j + | PEX _ j => env j | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2) | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2) | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index fccacc742..018b5c83f 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -947,7 +947,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). Fixpoint map_PExpr (e : PExpr S) : PExpr C := match e with | PEc c => PEc (C_of_S c) - | PEX p => PEX _ p + | PEX _ p => PEX _ p | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 440070a15..046c1b7cf 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -31,10 +31,10 @@ Set Implicit Arguments. Fixpoint eval_f (A:Type) (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop := match f with - | TT => True - | FF => False + | TT _ => True + | FF _ => False | A a => ev a - | X p => p + | X _ p => p | Cj e1 e2 => (eval_f ev e1) /\ (eval_f ev e2) | D e1 e2 => (eval_f ev e1) \/ (eval_f ev e2) | N e => ~ (eval_f ev e) @@ -54,9 +54,9 @@ Set Implicit Arguments. Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U := match f with - | TT => TT _ - | FF => FF _ - | X p => X _ p + | TT _ => TT _ + | FF _ => FF _ + | X _ p => X _ p | A a => A (fct a) | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2) | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2) @@ -172,9 +172,9 @@ Set Implicit Arguments. Fixpoint xcnf (pol : bool) (f : BFormula Term) {struct f}: cnf := match f with - | TT => if pol then tt else ff - | FF => if pol then ff else tt - | X p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) + | TT _ => if pol then tt else ff + | FF _ => if pol then ff else tt + | X _ p => if pol then ff else ff (* This is not complete - cannot negate any proposition *) | A x => if pol then normalise x else negate x | N e => xcnf (negb pol) e | Cj e1 e2 => diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index bdc4671df..d8ab6fd30 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -62,7 +62,7 @@ Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := match e with | PEc c => c - | PEX x => env x + | PEX _ x => env x | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2 | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2 | PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n) diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 4f4f20396..5c1f4c470 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -241,7 +241,7 @@ Fixpoint interpret3 t fv {struct t}: R := | (PEpow t1 t2) => let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2) | (PEc t1) => (IZR1 t1) - | (PEX n) => List.nth (pred (Pos.to_nat n)) fv 0 + | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0 end. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 341c0e6f5..2f30b6e17 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -407,7 +407,7 @@ Qed. Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := match e1, e2 with PEc c1, PEc c2 => ceqb c1 c2 - | PEX p1, PEX p2 => Pos.eqb p1 p2 + | PEX _ p1, PEX _ p2 => Pos.eqb p1 p2 | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 24c92b57f..7ffe98e29 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -419,7 +419,7 @@ Qed. Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := match pe with | PEc c => [c] - | PEX j => nth 0 j l + | PEX _ j => nth 0 j l | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) @@ -501,7 +501,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Fixpoint norm_aux (pe:PExpr C) : Pol := match pe with | PEc c => Pc c - | PEX j => mk_X j + | PEX _ j => mk_X j | PEadd pe1 (PEopp pe2) => Psub (norm_aux pe1) (norm_aux pe2) | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v index 947d15f0d..884ac01cd 100644 --- a/test-suite/bugs/closed/shouldsucceed/1834.v +++ b/test-suite/bugs/closed/shouldsucceed/1834.v @@ -53,7 +53,7 @@ Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := y1 e1. Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) := - match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end. + match E with exist _ e0 e1 => S1_1 y0 y1 e0 e1 = y2 end. Definition eq_2 y0 y1 y2 := {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}. @@ -81,7 +81,7 @@ Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) y2 e2. Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop := - match E with exist (exist e0 e1) e2 => + match E with exist _ (exist _ e0 e1) e2 => S2_2 y0 y1 y2 e0 e1 e2 = y3 end. Definition eq_3 y0 y1 y2 y3 := @@ -118,7 +118,7 @@ Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) y3 e3. Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop := - match E with exist (exist (exist e0 e1) e2) e3 => + match E with exist _ (exist _ (exist _ e0 e1) e2) e3 => S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end. Definition eq_4 y0 y1 y2 y3 y4 := @@ -165,7 +165,7 @@ Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) y4 e4. Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop := - match E with exist (exist (exist (exist e0 e1) e2) e3) e4 => + match E with exist _ (exist _ (exist _ (exist _ e0 e1) e2) e3) e4 => S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end. Definition eq_5 y0 y1 y2 y3 y4 y5 := diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v index 2d90a2f1d..685811176 100644 --- a/test-suite/bugs/closed/shouldsucceed/1891.v +++ b/test-suite/bugs/closed/shouldsucceed/1891.v @@ -7,7 +7,7 @@ Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. - refine (match x return _ with mkT n => fun g => f (g _) end). + refine (match x return _ with mkT _ n => fun g => f (g _) end). trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2353.v b/test-suite/bugs/closed/shouldsucceed/2353.v index b5c45c28c..baae9a6ec 100644 --- a/test-suite/bugs/closed/shouldsucceed/2353.v +++ b/test-suite/bugs/closed/shouldsucceed/2353.v @@ -4,9 +4,9 @@ Inductive term n := app (l : list term n). Definition term_list := fix term_size n (t : term n) (acc : nat) {struct t} : nat := match t with - | app l => + | app _ l => (fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat := match l with - | cons t q => term_list_size (S n) q (term_size n t acc) + | cons _ _ t q => term_list_size (S n) q (term_size n t acc) end) n l (S acc) end. diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v index 7deec64dd..ab39633f8 100644 --- a/test-suite/bugs/closed/shouldsucceed/2378.v +++ b/test-suite/bugs/closed/shouldsucceed/2378.v @@ -66,9 +66,9 @@ Implicit Arguments lpSat. Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := match f with - LPPred p => p2lp p - | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) - | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) + LPPred _ p => p2lp p + | LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) + | LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) end. Implicit Arguments LPTransfo. diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v index fe8eba549..8ac696e91 100644 --- a/test-suite/bugs/closed/shouldsucceed/2404.v +++ b/test-suite/bugs/closed/shouldsucceed/2404.v @@ -37,8 +37,8 @@ Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak. Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) := match aRWb,y with - | starReflS a, y' => Some y' - | starTransS i j k jWk jRWi, y' => + | starReflS _ a, y' => Some y' + | starTransS jWk jRWi, y' => match (bexportw jWk y) with | Some x => exportRweak jRWi x | None => None diff --git a/test-suite/bugs/closed/shouldsucceed/2729.v b/test-suite/bugs/closed/shouldsucceed/2729.v index 44f8d3c7c..3efca5d99 100644 --- a/test-suite/bugs/closed/shouldsucceed/2729.v +++ b/test-suite/bugs/closed/shouldsucceed/2729.v @@ -53,12 +53,12 @@ Program Fixpoint insertBase {pu : PatchUniverse} (qs : SequenceBase pu mid to) : SequenceBase pu from to := match qs with - | Nil _ => Cons p Nil - | Cons mid' mid2' to' q qs' => + | Nil => Cons p Nil + | Cons q qs' => match SignedName_compare (pu_nameOf p) (pu_nameOf q) with | Lt => Cons p qs | _ => match commutable_dec p (castPatchFrom _ q) with - | inleft (existT _ (existT q' (existT p' _))) => Cons q' + | inleft (existT _ _ (existT _ q' (existT _ p' _))) => Cons q' (insertBase p' qs') | inright _ => Cons p qs end diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v index 1845dd1f6..a0668cd19 100644 --- a/test-suite/bugs/opened/shouldnotfail/1501.v +++ b/test-suite/bugs/opened/shouldnotfail/1501.v @@ -40,11 +40,13 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Add Relation K equiv - reflexivity proved by (@equiv_refl) - symmetry proved by (@equiv_sym) - transitivity proved by (@equiv_trans) - as equiv_rel. +Instance equiv_rel A: Equivalence (@equiv A). +Proof. + constructor. + intros xa; apply equiv_refl. + intros xa xb; apply equiv_sym. + intros xa xb xc; apply equiv_trans. +Defined. Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g x)). @@ -67,17 +69,17 @@ Proof. unfold fequiv; intros; eapply equiv_trans; auto with monad. Qed. -Add Relation (fun (A B:Type) => A -> K B) fequiv - reflexivity proved by (@fequiv_refl) - symmetry proved by (@fequiv_sym) - transitivity proved by (@fequiv_trans) - as fequiv_rel. +Instance fequiv_re A B: Equivalence (@fequiv A B). +Proof. + constructor. + intros f; apply fequiv_refl. + intros f g; apply fequiv_sym. + intros f g h; apply fequiv_trans. +Defined. -Add Morphism bind - with signature equiv ==> fequiv ==> equiv - as bind_mor. +Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B). Proof. - unfold fequiv; intros; apply bind_compat; auto. + unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto. Qed. Lemma test: diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v index de77e35d3..22f61ab72 100644 --- a/test-suite/bugs/opened/shouldnotfail/1596.v +++ b/test-suite/bugs/opened/shouldnotfail/1596.v @@ -100,6 +100,16 @@ Definition t := (X.t * Y.t)%type. left;trivial. Defined. + Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. + Proof. + intros [xa xb] [ya yb]; simpl. + destruct (X.eq_dec xa ya). + destruct (Y.eq_dec xb yb). + + left; now split. + + right. now intros [eqa eqb]. + + right. now intros [eqa eqb]. + Defined. + Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. End OrderedPair. @@ -158,6 +168,14 @@ GT;simpl;trivial;fail). apply GT;trivial. Defined. + Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. + Proof. + intros [i] [j]. unfold eq. + destruct (eq_nat_dec i j). + + left. now f_equal. + + right. intros meq; now inversion meq. + Defined. + Hint Immediate eq_sym. Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. End Ord. diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v index d63c49403..ec4852300 100644 --- a/test-suite/failure/Case9.v +++ b/test-suite/failure/Case9.v @@ -2,7 +2,9 @@ Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. Type match compare 0 0 return nat with - (* k<i *) | left _ _ (left _ _ _) => 0 - (* k=i *) | left _ _ _ => 0 - (* k>i *) | right _ _ _ => 0 + (* k<i *) | left _ (left _ _) => 0 + (* k=i *) | left _ _ => 0 + (* k>i *) | right _ _ => 0 + end. + end. diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 324dc6030..cd3c81f49 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -5,9 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - +(* Fixpoint F (n:nat) : False := F (match F n with end). - +*) (* de Bruijn mix-up *) (* If accepted, Eval compute in f 0. loops *) Definition f := diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 341805a16..7214287a6 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -145,8 +145,8 @@ Module ListDict (E: ELEM). Definition add (e : elt) (s : T) := cons elt e s. Fixpoint find (e : elt) (s : T) {struct s} : bool := match s with - | nil => false - | cons e' s' => ifte (E.eq_dec e e') true (find e s') + | nil _ => false + | cons _ e' s' => ifte (E.eq_dec e e') true (find e s') end. Definition find_empty_false (e : elt) := refl_equal false. diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f5610efc4..6c514b16e 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -22,8 +22,8 @@ Inductive hole (A:Set) : Set := Hole | Hole2. Definition wrong_id (A B : Set) (x:hole A) : hole B := match x with - | Hole => @Hole _ - | Hole2 => @Hole2 _ + | Hole _ => @Hole _ + | Hole2 _ => @Hole2 _ end. Extraction wrong_id. (** should _not_ be optimized as an identity *) @@ -114,9 +114,9 @@ Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode) | Some oc => match f w with | DecInst i => DecInst (g i oc) - | DecError m => @DecError inst m - | DecUndefined => @DecUndefined inst - | DecUnpredictable => @DecUnpredictable inst + | DecError _ m => @DecError inst m + | DecUndefined _ => @DecUndefined inst + | DecUnpredictable _ => @DecUnpredictable inst end | None => @DecUndefined inst end. diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v index c8f772687..445ffac8c 100644 --- a/test-suite/success/Case11.v +++ b/test-suite/success/Case11.v @@ -7,7 +7,7 @@ Variables (Alpha : Set) (Beta : Set). Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) : Alpha * Beta := match c with - | existS a b => (a, b) + | existS _ a b => (a, b) end. End A. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v index 729ab824f..55e17facc 100644 --- a/test-suite/success/Case12.v +++ b/test-suite/success/Case12.v @@ -68,6 +68,6 @@ Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set := Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) {struct l} : nat := match l with - | nil''' => 0 - | cons''' _ m l0 => S (length''' A a m l0) + | nil''' _ _ => 0 + | @cons''' _ _ _ _ m l0 => S (length''' A a m l0) end. diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v index 77016bbfe..ce9a0ecb4 100644 --- a/test-suite/success/Case16.v +++ b/test-suite/success/Case16.v @@ -5,6 +5,6 @@ Check (fun x : {b : bool | if b then True else False} => match x return (let (b, _) := x in if b then True else False) with - | exist true y => y - | exist false z => z + | exist _ true y => y + | exist _ false z => z end). diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 66af9e0d3..861d04668 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A. Check (match rec l0 (HHH _) with - | inleft (existS (false :: l1) _) => inright _ (HHH _) - | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + | inleft (existS _ (false :: l1) _) => inright _ (HHH _) + | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _) => inright _ (HHH _) + | inleft (existS _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & @@ -39,10 +39,10 @@ Check {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) => match rec l0 (HHH _) with - | inleft (existS (false :: l1) _) => inright _ (HHH _) - | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + | inleft (existS _ (false :: l1) _) => inright _ (HHH _) + | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _) => inright _ (HHH _) + | inleft (existS _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v index 6e4b20031..f95598aad 100644 --- a/test-suite/success/Case7.v +++ b/test-suite/success/Case7.v @@ -12,6 +12,6 @@ Parameter Type (fun (A : Set) (l : List A) => match l return (Empty A l \/ ~ Empty A l) with - | Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A) - | Cons a y as b => or_intror (Empty A b) (inv_Empty A a y) + | Nil _ => or_introl (~ Empty A (Nil A)) (intro_Empty A) + | Cons _ a y as b => or_intror (Empty A b) (inv_Empty A a y) end). diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v index a8534a0b9..e34e5b9ba 100644 --- a/test-suite/success/Case9.v +++ b/test-suite/success/Case9.v @@ -36,10 +36,10 @@ Parameter Fixpoint eqlongdec (x y : List nat) {struct x} : eqlong x y \/ ~ eqlong x y := match x, y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil - | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) - | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) - | Cons a x as L1, Cons b y as L2 => + | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons _ a x as L1, Cons _ b y as L2 => match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) @@ -49,10 +49,10 @@ Fixpoint eqlongdec (x y : List nat) {struct x} : Type match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil - | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) - | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) - | Cons a x as L1, Cons b y as L2 => + | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons _ a x as L1, Cons _ b y as L2 => match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v index 543ca0c92..cf102486a 100644 --- a/test-suite/success/Cases-bug1834.v +++ b/test-suite/success/Cases-bug1834.v @@ -7,7 +7,7 @@ Definition T := sig P. Parameter Q : T -> Prop. Definition U := sig Q. Parameter a : U. -Check (match a with exist (exist tt e2) e3 => e3=e3 end). +Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end). (* There is still a form submitted by Pierre Corbineau (#1834) which fails *) diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index c9a3c08ef..257c55fd8 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -309,43 +309,43 @@ Type Type (fun l : List nat => match l return (List nat) with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end). Type (fun l : List nat => match l with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end). Type match Nil nat return nat with - | Nil => 0 - | Cons a l => S a + | Nil _ => 0 + | Cons _ a l => S a end. Type match Nil nat with - | Nil => 0 - | Cons a l => S a + | Nil _ => 0 + | Cons _ a l => S a end. Type match Nil nat return (List nat) with - | Cons a l => l + | Cons _ a l => l | x => x end. Type match Nil nat with - | Cons a l => l + | Cons _ a l => l | x => x end. Type match Nil nat return (List nat) with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end. Type match Nil nat with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end. @@ -353,8 +353,8 @@ Type match 0 return nat with | O => 0 | S x => match Nil nat return nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end. @@ -362,8 +362,8 @@ Type match 0 with | O => 0 | S x => match Nil nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end. @@ -372,8 +372,8 @@ Type match y with | O => 0 | S x => match Nil nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end). @@ -381,8 +381,8 @@ Type Type match 0, Nil nat return nat with | O, x => 0 - | S x, Nil => x - | S x, Cons a l => x + a + | S x, Nil _ => x + | S x, Cons _ a l => x + a end. @@ -597,71 +597,60 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return nat with - | Niln => 0 - | Consn n a Niln => 0 - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => 0 + | Consn _ n a (Consn _ m b l) => n + m end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => 0 - | Consn n a Niln => 0 - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => 0 + | Consn _ n a (Consn _ m b l) => n + m end). -(* This example was deactivated in Cristina's code - Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A O with - | Niln as b => b - | Consn n a (Niln as b) => (Niln A) - | Consn n a (Consn m b l) => (Niln A) + | Niln _ as b => b + | Consn _ n a (Niln _ as b) => (Niln A) + | Consn _ n a (Consn _ m b l) => (Niln A) end). -*) - -(* This one is (still) failing: too weak unification +(* Type (fun (A:Set) (n:nat) (l:Listn A n) => match l with - | Niln as b => b - | Consn n a (Niln as b) => (Niln A) - | Consn n a (Consn m b l) => (Niln A) + | Niln _ as b => b + | Consn _ n a (Niln _ as b) => (Niln A) + | Consn _ n a (Consn _ m b l) => (Niln A) end). *) -(* This one is failing: alias L not chosen of the right type - Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A (S 0) with - | Niln as b => Consn A O O b - | Consn n a Niln as L => L - | Consn n a _ => Consn A O O (Niln A) + | Niln _ as b => Consn A O O b + | Consn _ n a (Niln _) as L => L + | Consn _ n a _ => Consn A O O (Niln A) end). -*) - -(******** This example (still) failed Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A (S 0) with - | Niln as b => Consn A O O b - | Consn n a Niln as L => L - | Consn n a _ => Consn A O O (Niln A) + | Niln _ as b => Consn A O O b + | Consn _ n a (Niln _) as L => L + | Consn _ n a _ => Consn A O O (Niln A) end). -**********) - (* To test treatment of as-patterns in depth *) Type (fun (A : Set) (l : List A) => match l with - | Nil as b => Nil A - | Cons a Nil as L => L - | Cons a (Cons b m) as L => L + | Nil _ as b => Nil A + | Cons _ a (Nil _) as L => L + | Cons _ a (Cons _ b m) as L => L end). @@ -704,40 +693,40 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln as b => l + | Niln _ as b => l | _ => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (Listn A n) with - | Niln => l - | Consn n a Niln => l - | Consn n a (Consn m b c) => l + | Niln _ => l + | Consn _ n a (Niln _) => l + | Consn _ n a (Consn _ m b c) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => l - | Consn n a Niln => l - | Consn n a (Consn m b c) => l + | Niln _ => l + | Consn _ n a (Niln _) => l + | Consn _ n a (Consn _ m b c) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (Listn A n) with - | Niln as b => l - | Consn n a (Niln as b) => l - | Consn n a (Consn m b _) => l + | Niln _ as b => l + | Consn _ n a (Niln _ as b) => l + | Consn _ n a (Consn _ m b _) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln as b => l - | Consn n a (Niln as b) => l - | Consn n a (Consn m b _) => l + | Niln _ as b => l + | Consn _ n a (Niln _ as b) => l + | Consn _ n a (Consn _ m b _) => l end). @@ -770,40 +759,40 @@ Type match LeO 0 with Type (fun (n : nat) (l : Listn nat n) => match l return nat with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end). Type (fun (n : nat) (l : Listn nat n) => match l with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end). Type match Niln nat with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end. Type match LE_n 0 return nat with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. @@ -825,16 +814,17 @@ Type Type match Niln nat return nat with - | Niln => 0 - | Consn n a Niln => n - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _ +) => n + | Consn _ n a (Consn _ m b l) => n + m end. Type match Niln nat with - | Niln => 0 - | Consn n a Niln => n - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => n + | Consn _ n a (Consn _ m b l) => n + m end. @@ -1027,17 +1017,17 @@ Type Type match LE_n 0 return nat with - | LE_n => 0 - | LE_S m LE_n => 0 + m - | LE_S m (LE_S y h) => 0 + m + | LE_n _ => 0 + | LE_S _ m (LE_n _) => 0 + m + | LE_S _ m (LE_S _ y h) => 0 + m end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m LE_n => 0 + m - | LE_S m (LE_S y h) => 0 + m + | LE_n _ => 0 + | LE_S _ m (LE_n _) => 0 + m + | LE_S _ m (LE_S _ y h) => 0 + m end. @@ -1077,25 +1067,25 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (nat -> nat) with - | Niln => fun _ : nat => 0 - | Consn n a Niln => fun _ : nat => n - | Consn n a (Consn m b l) => fun _ : nat => n + m + | Niln _ => fun _ : nat => 0 + | Consn _ n a (Niln _) => fun _ : nat => n + | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => fun _ : nat => 0 - | Consn n a Niln => fun _ : nat => n - | Consn n a (Consn m b l) => fun _ : nat => n + m + | Niln _ => fun _ : nat => 0 + | Consn _ n a (Niln _) => fun _ : nat => n + | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m end). (* Also tests for multiple _ patterns *) Type (fun (A : Set) (n : nat) (l : Listn A n) => match l in (Listn _ n) return (Listn A n) with - | Niln as b => b - | Consn _ _ _ as b => b + | Niln _ as b => b + | Consn _ _ _ _ as b => b end). (** This one was said to raised once an "Horrible error message!" *) @@ -1103,8 +1093,8 @@ Type Type (fun (A:Set) (n:nat) (l:Listn A n) => match l with - | Niln as b => b - | Consn _ _ _ as b => b + | Niln _ as b => b + | Consn _ _ _ _ as b => b end). Type @@ -1123,26 +1113,26 @@ Type Type (fun (n m : nat) (h : LE n m) => match h return (nat -> nat) with - | LE_n => fun _ : nat => n - | LE_S m LE_n => fun _ : nat => n + m - | LE_S m (LE_S y h) => fun _ : nat => m + y + | LE_n _ => fun _ : nat => n + | LE_S _ m (LE_n _) => fun _ : nat => n + m + | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y end). Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => fun _ : nat => n - | LE_S m LE_n => fun _ : nat => n + m - | LE_S m (LE_S y h) => fun _ : nat => m + y + | LE_n _ => fun _ : nat => n + | LE_S _ m (LE_n _) => fun _ : nat => n + m + | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y end). Type (fun (n m : nat) (h : LE n m) => match h return nat with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y LE_n) => n + m + y - | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y + | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y') end). @@ -1150,28 +1140,28 @@ Type Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y LE_n) => n + m + y - | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y + | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y') end). Type (fun (n m : nat) (h : LE n m) => match h return nat with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y h) => n + m + y + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y h) => n + m + y end). Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y h) => n + m + y + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y h) => n + m + y end). Type @@ -1231,14 +1221,14 @@ Parameter B : Set. Type (fun (P : nat -> B -> Prop) (x : SStream B P) => match x return B with - | scons _ a _ _ => a + | scons _ _ a _ _ => a end). Type (fun (P : nat -> B -> Prop) (x : SStream B P) => match x with - | scons _ a _ _ => a + | scons _ _ a _ _ => a end). Type match (0, 0) return (nat * nat) with @@ -1267,14 +1257,14 @@ Parameter concat : forall A : Set, List A -> List A -> List A. Type match Nil nat, Nil nat return (List nat) with - | Nil as b, x => concat nat b x - | Cons _ _ as d, Nil as c => concat nat d c + | Nil _ as b, x => concat nat b x + | Cons _ _ _ as d, Nil _ as c => concat nat d c | _, _ => Nil nat end. Type match Nil nat, Nil nat with - | Nil as b, x => concat nat b x - | Cons _ _ as d, Nil as c => concat nat d c + | Nil _ as b, x => concat nat b x + | Cons _ _ _ as d, Nil _ as c => concat nat d c | _, _ => Nil nat end. @@ -1415,7 +1405,7 @@ Parameter p : eq_prf. Type match p with - | ex_intro c eqc => + | ex_intro _ c eqc => match eq_nat_dec c n with | right _ => refl_equal n | left y => (* c=n*) refl_equal n @@ -1438,7 +1428,7 @@ Type (fun N : nat => match N_cla N with | inright H => match exist_U2 N H with - | exist a b => a + | exist _ a b => a end | _ => 0 end). @@ -1636,8 +1626,8 @@ Parameter Type match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with - | Nil => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat) - | Cons a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y) + | Nil _ => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat) + | Cons _ a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y) end. @@ -1687,20 +1677,20 @@ Parameter Type match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => V1 - | Nil, Cons a x => V2 a x - | Cons a x, Nil => V3 a x - | Cons a x, Cons b y => V4 a x b y + | Nil _, Nil _ => V1 + | Nil _, Cons _ a x => V2 a x + | Cons _ a x, Nil _ => V3 a x + | Cons _ a x, Cons _ b y => V4 a x b y end. Type (fun x y : List nat => match x, y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => V1 - | Nil, Cons a x => V2 a x - | Cons a x, Nil => V3 a x - | Cons a x, Cons b y => V4 a x b y + | Nil _, Nil _ => V1 + | Nil _, Cons _ a x => V2 a x + | Cons _ a x, Nil _ => V3 a x + | Cons _ a x, Cons _ b y => V4 a x b y end). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index bfead53c0..8d9edbd62 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -4,8 +4,8 @@ Check (fun (P : nat -> Prop) Q (A : P 0 -> Q) (B : forall n : nat, P (S n) -> Q) x => match x return Q with - | exist O H => A H - | exist (S n) H => B n H + | exist _ O H => A H + | exist _ (S n) H => B n H end). (* Check dependencies in anonymous arguments (from FTA/listn.v) *) @@ -21,30 +21,30 @@ Variable c : C. Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := match bs with - | niln => c - | consn b _ tl => g b (foldrn _ tl) + | niln _ => c + | consn _ b _ tl => g b (foldrn _ tl) end. End Folding. (** Testing post-processing of nested dependencies *) Check fun x:{x|x=0}*nat+nat => match x with - | inl ((exist 0 eq_refl),0) => None + | inl ((exist _ 0 eq_refl),0) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. @@ -52,11 +52,11 @@ Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with - | exist2 (x,y) eq_refl I => None + | exist2 _ _ (x,y) eq_refl I => None end. Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with - | inl (exist (exist2 (x,y) eq_refl I) I) => None + | inl (exist _ (exist2 _ _ (x,y) eq_refl I) I) => None | _ => Some 0 end. @@ -521,8 +521,8 @@ end. Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) := match v with - | niln => w - | consn a n' v' => consn _ a _ (app v' w) + | niln _ => w + | consn _ a n' v' => consn _ a _ (app v' w) end. (* Testing regression of bug 2106 *) @@ -547,7 +547,7 @@ n'. Definition test (s:step E E) := match s with - | Step nil _ (cons E nil) _ Plus l l' => true + | @Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 3a4f88993..5fc703cf0 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -42,8 +42,8 @@ Variables (B C : Set) (g : B -> C -> C) (c : C). Fixpoint foldrn n bs := match bs with - | Vnil => c - | Vcons b _ tl => g b (foldrn _ tl) + | Vnil _ => c + | Vcons _ b _ tl => g b (foldrn _ tl) end. End folding. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 84ec298df..a654080de 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -9,11 +9,11 @@ Require Import Coq.Program.Program. Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n := match v with | vnil => ! - | vcons a n' v' => v' + | vcons a v' => v' end. Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) := match v in vector _ n return vector A (n + m) with | vnil => w - | vcons a n' v' => vcons a (app v' w) + | vcons a v' => vcons a (app v' w) end. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 59aa87de4..5e59930f3 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -38,7 +38,7 @@ Check (f : forall z : C, P z (I C D x y z)) (y0 : C) (a : A C D x y y0) => match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with - | I x0 => f x0 + | I _ _ _ _ x0 => f x0 end). Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set := {p : C; q : E}. @@ -51,7 +51,7 @@ Check (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) (b : B C D x y) => match b as b0 return (P b0) with - | Build_B x0 x1 => f x0 x1 + | Build_B _ _ _ _ x0 x1 => f x0 x1 end). (* Check inductive types with local definitions (constructors) *) diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v index 4c790680d..0e557aee0 100644 --- a/test-suite/success/LetPat.v +++ b/test-suite/success/LetPat.v @@ -9,22 +9,22 @@ Print l3. Record someT (A : Type) := mkT { a : nat; b: A }. -Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x. +Definition l4 A (t : someT A) : nat := let 'mkT _ x y := t in x. Print l4. Print sigT. Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y := t return B (projT1 t) in y. + let 'existT _ x y := t return B (projT1 t) in y. Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y as t' := t return B (projT1 t') in y. + let 'existT _ x y as t' := t return B (projT1 t') in y. Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y as t' in sigT _ := t return B (projT1 t') in y. + let 'existT _ x y as t' in sigT _ := t return B (projT1 t') in y. Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := match t with - existT x y => y + existT _ x y => y end. (** An example from algebra, using let' and inference of return clauses diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 459645f6f..15af08442 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -301,8 +301,8 @@ Section Le_case_analysis. (HS : forall m, n <= m -> Q (S m)). Check ( match H in (_ <= q) return (Q q) with - | le_n => H0 - | le_S m Hm => HS m Hm + | le_n _ => H0 + | le_S _ m Hm => HS m Hm end ). @@ -320,8 +320,8 @@ Qed. Definition Vtail_total (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with -| Vector.nil => Vector.nil A -| Vector.cons _ n0 v0 => v0 +| Vector.nil _ => Vector.nil A +| Vector.cons _ _ n0 v0 => v0 end. Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). @@ -1060,8 +1060,8 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with _ , Vector.nil => None - | 0 , Vector.cons b _ _ => Some b - | S n', Vector.cons _ p' v' => vector_nth A n' p' v' + | 0 , Vector.cons b _ => Some b + | S n', Vector.cons _ v' => vector_nth A n' _ v' end. Implicit Arguments vector_nth [A p]. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 4292ecb6a..b538d2ed2 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -96,13 +96,13 @@ Inductive list (A : Type) : Type := nil : list A | cons : A -> list A -> list A. Inductive vect (A : Type) : nat -> Type := vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n). -Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end. +Fixpoint size A (l : list A) : nat := match l with nil _ => 0 | cons _ _ tl => 1+size _ tl end. Section test_non_unif_but_complete. Fixpoint l2v A (l : list A) : vect A (size A l) := match l as l return vect A (size A l) with - | nil => vnil A - | cons x xs => vcons A (size A xs) x (l2v A xs) + | nil _ => vnil A + | cons _ x xs => vcons A (size A xs) x (l2v A xs) end. Local Coercion l2v : list >-> vect. @@ -121,8 +121,8 @@ Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := match l as l return vect B (size A l) with - | nil => vnil B - | cons x xs => vcons _ _ (c x) (l2v2 xs) end. + | nil _ => vnil B + | cons _ x xs => vcons _ _ (c x) (l2v2 xs) end. Local Coercion l2v2 : list >-> vect. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index ff8b28bae..0e7d653b4 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -51,7 +51,7 @@ Check (let p := fun (m : nat) f (n : nat) => match f m n with - | exist a b => exist _ a b + | exist _ a b => exist _ a b end in p :forall x : nat, @@ -178,9 +178,9 @@ refine | left _ => _ | right _ => match le_step s _ _ with - | exist s' h' => + | exist _ s' h' => match hr s' _ _ with - | exist s'' _ => exist _ s'' _ + | exist _ s'' _ => exist _ s'' _ end end end)). @@ -204,7 +204,7 @@ Abort. Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := match l with | nil => nil - | (existT k v)::l' => (existT _ k v):: (filter A l') + | (existT _ k v)::l' => (existT _ k v):: (filter A l') end. (* Bug #2000: used to raise Out of memory in 8.2 while it should fail by diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 8b4f41055..352abb2af 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -84,7 +84,7 @@ Definition div : refine (fun m div_rec n => match div_rec m n with - | exist _ _ => _ + | exist _ _ _ => _ end). Abort. 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 |