diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Ints/Int31.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/theories/Ints/Int31.v b/theories/Ints/Int31.v index 59e45c320..918c54232 100644 --- a/theories/Ints/Int31.v +++ b/theories/Ints/Int31.v @@ -402,4 +402,7 @@ Definition tail031 (i:int31) := | D1 => n end) i On -.
\ No newline at end of file +. + +Register head031 as int31 head0 in "coq_int31" by True. +Register tail031 as int31 tail0 in "coq_int31" by True. |