diff options
Diffstat (limited to 'test-suite/tactics')
| -rw-r--r-- | test-suite/tactics/TestRefine.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v index b8c0146e84..f752c5bc6f 100644 --- a/test-suite/tactics/TestRefine.v +++ b/test-suite/tactics/TestRefine.v @@ -1,17 +1,17 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (* Petit bench vite fait, mal fait *) Require Refine. -(***********************************************************************) +(************************************************************************) Lemma essai : (x:nat)x=x. @@ -37,7 +37,7 @@ Refine [x0:nat]Cases x0 of O => ? | (S p) => ? end. (* cannot be executed *) Abort. -(***********************************************************************) +(************************************************************************) Lemma T : nat. @@ -46,7 +46,7 @@ Refine (S ?). Abort. -(***********************************************************************) +(************************************************************************) Lemma essai2 : (x:nat)x=x. @@ -79,7 +79,7 @@ Refine Fix f{f/1 : (x:nat)x=x := Abort. -(***********************************************************************) +(************************************************************************) Lemma essai : nat. @@ -94,7 +94,7 @@ Refine (f ? O). Abort. -(***********************************************************************) +(************************************************************************) Parameter P : nat -> Prop. @@ -115,7 +115,7 @@ Refine (exist nat [x:nat](x=(S O)) (S O) ?). Abort. -(***********************************************************************) +(************************************************************************) Lemma essai : (n:nat){ x:nat | x=(S n) }. |