From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/CasesDep.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'test-suite/success/CasesDep.v') diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index bfead53c..8d9edbd6 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. -- cgit v1.2.3