tail0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9877 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v
index 8a19e878d3..59e45c320a 100644
--- a/theories/Ints/Int31.v
+++ b/theories/Ints/Int31.v
@@ -394,4 +394,12 @@ Definition head031 (i:int31) :=
                                           | D1 => n
                                           end)
        i On
+.
+
+Definition tail031 (i:int31) :=
+  recr _ (fun _ => T31) (fun b si rec n => match b with 
+                                          | D0 => rec (add31 n In)
+                                          | D1 => n
+                                          end)
+       i On
 .
\ No newline at end of file