diff options
Diffstat (limited to 'contrib/subtac/test/ListsTest.v')
-rw-r--r-- | contrib/subtac/test/ListsTest.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index a29cd039..8429c267 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -5,12 +5,13 @@ Variable A : Set. Program Definition myhd : forall { l : list A | length l <> 0 }, A := fun l => - match l with + match `l with | nil => _ | hd :: tl => hd end. Proof. - destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition. + destruct l ; simpl ; intro H. + rewrite H in n ; intuition. Defined. @@ -24,7 +25,7 @@ Program Definition mytail : forall { l : list A | length l <> 0 }, list A := | hd :: tl => tl end. Proof. -destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition. +destruct l ; simpl ; intro H ; rewrite H in n ; intuition. Defined. Extraction mytail. @@ -50,7 +51,6 @@ Program Fixpoint append (l : list A) (l' : list A) { struct l } : | nil => l' | hd :: tl => hd :: (append tl l') end. -simpl. subst ; auto. simpl ; rewrite (subset_simpl (append tl0 l')). simpl ; subst. |