diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
commit | 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 (patch) | |
tree | c160d442d54dbd15cbd0ab3500cdf94d0a6da74e /test-suite/success/refine.v | |
parent | 960859c0c10e029f9768d0d70addeca8f6b6d784 (diff) |
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/refine.v')
-rw-r--r-- | test-suite/success/refine.v | 59 |
1 files changed, 31 insertions, 28 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 96fa79ebd..b61cf275f 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -1,33 +1,34 @@ (* Refine and let-in's *) -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in ?. -Exists y; Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in _). +exists y; auto. Save test1. -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?). -Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in ex_intro _ (y + y) _). +auto. Save test2. Goal nat. -Refine let y = O in (plus O ?). -Exact (S O). + refine (let y := 0 in 0 + _). +exact 1. Save test3. (* Example submitted by Yves on coqdev *) -Require PolyList. +Require Import List. -Goal (l:(list nat))l=l. +Goal forall l : list nat, l = l. Proof. -Refine [l]<[l]l=l> - Cases l of - | nil => ? - | (cons O l0) => ? - | (cons (S _) l0) => ? - end. + refine + (fun l => + match l return (l = l) with + | nil => _ + | O :: l0 => _ + | S _ :: l0 => _ + end). Abort. (* Submitted by Roland Zumkeller (bug #888) *) @@ -36,10 +37,10 @@ Abort. (co-)fixpoint *) Goal nat -> nat. -Refine( - Fix f {f [n:nat] : nat := (S ?) with - pred [n:nat] : nat := n}). -Exact 0. + refine (fix f (n : nat) : nat := S _ + with pred (n : nat) : nat := n + for f). +exact 0. Qed. (* Submitted by Roland Zumkeller (bug #889) *) @@ -47,17 +48,19 @@ Qed. (* The types of metas were in metamap and they were not updated when passing through a binder *) -Goal (n:nat) nat -> n=0. -Refine [n] - Fix f { f [i:nat] : n=0 := - Cases i of 0 => ? | (S _) => ? end }. +Goal forall n : nat, nat -> n = 0. + refine + (fun n => fix f (i : nat) : n = 0 := match i with + | O => _ + | S _ => _ + end). Abort. (* Submitted by Roland Zumkeller (bug #931) *) (* Don't turn dependent evar into metas *) -Goal ((n:nat)n=O->Prop) -> Prop. -Intro P. -Refine(P ? ?). -Reflexivity. +Goal (forall n : nat, n = 0 -> Prop) -> Prop. +intro P. + refine (P _ _). +reflexivity. Abort. |