Non-empty-diff: diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs index 8a7afcd..73dc28f 100644 --- a/fiat-rust/src/curve25519_64.rs +++ b/fiat-rust/src/curve25519_64.rs @@ -15,13 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] -/* fiat_25519_u1 represents one byte. */ +/** fiat_25519_u1 represents values of 1 bits, stored in one byte. */ pub type fiat_25519_u1 = u8; -/* fiat_25519_i1 represents one byte. */ +/** fiat_25519_i1 represents values of 1 bits, stored in one byte. */ pub type fiat_25519_i1 = i8; -/* fiat_25519_u2 represents one byte. */ +/** fiat_25519_u2 represents values of 2 bits, stored in one byte. */ pub type fiat_25519_u2 = u8; -/* fiat_25519_i2 represents one byte. */ +/** fiat_25519_i2 represents values of 2 bits, stored in one byte. */ pub type fiat_25519_i2 = i8; /** The type fiat_25519_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/p448_solinas_32.rs b/fiat-rust/src/p448_solinas_32.rs index 6bc3509..5673ee1 100644 --- a/fiat-rust/src/p448_solinas_32.rs +++ b/fiat-rust/src/p448_solinas_32.rs @@ -15,13 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] -/* fiat_p448_u1 represents one byte. */ +/** fiat_p448_u1 represents values of 1 bits, stored in one byte. */ pub type fiat_p448_u1 = u8; -/* fiat_p448_i1 represents one byte. */ +/** fiat_p448_i1 represents values of 1 bits, stored in one byte. */ pub type fiat_p448_i1 = i8; -/* fiat_p448_u2 represents one byte. */ +/** fiat_p448_u2 represents values of 2 bits, stored in one byte. */ pub type fiat_p448_u2 = u8; -/* fiat_p448_i2 represents one byte. */ +/** fiat_p448_i2 represents values of 2 bits, stored in one byte. */ pub type fiat_p448_i2 = i8; /** The type fiat_p448_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/p448_solinas_64.rs b/fiat-rust/src/p448_solinas_64.rs index 7d23c13..d315e37 100644 --- a/fiat-rust/src/p448_solinas_64.rs +++ b/fiat-rust/src/p448_solinas_64.rs @@ -15,13 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] -/* fiat_p448_u1 represents one byte. */ +/** fiat_p448_u1 represents values of 1 bits, stored in one byte. */ pub type fiat_p448_u1 = u8; -/* fiat_p448_i1 represents one byte. */ +/** fiat_p448_i1 represents values of 1 bits, stored in one byte. */ pub type fiat_p448_i1 = i8; -/* fiat_p448_u2 represents one byte. */ +/** fiat_p448_u2 represents values of 2 bits, stored in one byte. */ pub type fiat_p448_u2 = u8; -/* fiat_p448_i2 represents one byte. */ +/** fiat_p448_i2 represents values of 2 bits, stored in one byte. */ pub type fiat_p448_i2 = i8; /** The type fiat_p448_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs index 6686702..7ed2283 100644 --- a/fiat-rust/src/poly1305_32.rs +++ b/fiat-rust/src/poly1305_32.rs @@ -15,13 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] -/* fiat_poly1305_u1 represents one byte. */ +/** fiat_poly1305_u1 represents values of 1 bits, stored in one byte. */ pub type fiat_poly1305_u1 = u8; -/* fiat_poly1305_i1 represents one byte. */ +/** fiat_poly1305_i1 represents values of 1 bits, stored in one byte. */ pub type fiat_poly1305_i1 = i8; -/* fiat_poly1305_u2 represents one byte. */ +/** fiat_poly1305_u2 represents values of 2 bits, stored in one byte. */ pub type fiat_poly1305_u2 = u8; -/* fiat_poly1305_i2 represents one byte. */ +/** fiat_poly1305_i2 represents values of 2 bits, stored in one byte. */ pub type fiat_poly1305_i2 = i8; /** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */ diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs index 7d9c566..81fe43b 100644 --- a/fiat-rust/src/poly1305_64.rs +++ b/fiat-rust/src/poly1305_64.rs @@ -15,13 +15,13 @@ #![allow(unused_parens)] #![allow(non_camel_case_types)] -/* fiat_poly1305_u1 represents one byte. */ +/** fiat_poly1305_u1 represents values of 1 bits, stored in one byte. *

Process completed with exit code 1.

Makefile.coq:793: src/Coqprime/Tactic/Tactic.v

Makefile.coq.noex:793: D:/a/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.v

Makefile.coq.noex:409: all

Makefile:42: noex