diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index ba40ffd87c..b3a985b63b 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -43,7 +43,7 @@ Inductive int31 : Type := I31 : nfun digits size int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault - occur when they are applied to one non-closed term and one closed term *) + occur when they are applied to one non-closed term and one closed term). *) Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. |