driver. We hook into the compiler by implementing the Callbacks trait. The implementation is located is in the flux-driver crate, and it is the main entry point to Flux.
flux-attrs: Implementation of user facing procedural macros for annotating programs with Flux specs.
-
flux-attrs-proc-macros: Procedural macro crate exporting the user facing procedural macros.
-
flux-attrs-proc-macros-build: Dummy crate used to pre-build the procedural macro crate with relevant features enabled. The main purpose of this crate is being able to use procedural macros in tests.
-
flux-bin: Contains the cargo-flux and rustc-flux binaries.
-
flux-common: Common utility definitions used across all crates.
-
flux-config: Crate containing logic associated with global configuration Flags that change the behavior of Flux, e.g, to enable or disable overflow checking.
-
flux-desugar: Implementation of name resolution and desugaring from Flux surface syntax into Flux high-level intermediate representation (fhir).
-
flux-driver: Main entry point to Flux. It contains the implementation of the Callbacks trait.
-
flux-errors: Utility definitions for user facing error reporting.
-
flux-fhir-analysis: Implements the "analyses" performed in the fhir, most notably well-formedness checking and conversion from fhir into rty.
-
flux-fixpoint: Code to interact with the Liquid Fixpoint binary.
-
flux-macros: Procedural macros used internally to implement Flux.
-
flux-metadata: Logic for saving Flux crate metadata that can be used to import refined signatures from external crates.
-
flux-middle: This crate contains common type definitions that are used by the rest of Flux like the rty and fhir intermediate representations. Akin to rustc_middle.
-
flux-refineck: Implementation of refinement type checking.
-
flux-syntax: Definition of the surface syntax AST and parser.
-
flux-tests: Flux regression tests.
+
crates/flux-bin: Contains the cargo-flux and rustc-flux binaries used to launch the flux-driver.
+
crates/flux-common: Common utility definitions used across all crates.
+
crates/flux-config: Crate containing logic associated with global configuration flags that change the behavior of Flux, e.g, to enable or disable overflow checking.
+
crates/flux-desugar: Implementation of name resolution and desugaring from Flux surface syntax into Flux high-level intermediate representation (fhir). This includes name resolution.
+
crates/flux-driver: Main entry point to Flux. It contains the flux-driver binary and the implementation of the Callbacks trait.
+
crates/flux-errors: Utility definitions for user facing error reporting.
+
crates/flux-fhir-analysis: Implements the "analyses" performed in the fhir, most notably well-formedness checking and conversion from fhir into rty.
+
crates/flux-fixpoint: Code to interact with the Liquid Fixpoint binary.
+
crates/flux-macros: Procedural macros used internally to implement Flux.
+
crates/flux-metadata: Logic for saving Flux crate metadata that can be used to import refined signatures from external crates.
+
crates/flux-middle: This crate contains common type definitions that are used by the rest of Flux like the rty and fhir intermediate representations. Akin to rustc_middle.
+
crates/flux-refineck: Implementation of refinement type checking.
+
crates/flux-syntax: Definition of the surface syntax AST and parser.
+
crates/flux-tests: Flux regression tests.
+
lib/flux-attrs: Implementation of user facing procedural macros for annotating programs with Flux specs.
+
lib/flux-rs: This is just a re-export of the macros implemented in flux-attrs. The intention is to eventually put Flux "standard library" here, i.e., a set of definitions that are useful when working with Flux.
Flux has several intermediate representations (IR) for types. They represent a refined version of an equivalent type in some rustc IR. We have picked a distinct verb to refer to the process of going between these different representations to make it easier to refer to them. The following image summarizes all the IRs and the process for going between them.
diff --git a/doc/flux_fixpoint/all.html b/doc/flux_fixpoint/all.html
index f20c40f90c..24d78f3911 100644
--- a/doc/flux_fixpoint/all.html
+++ b/doc/flux_fixpoint/all.html
@@ -1 +1 @@
-List of all items in this crate
\ No newline at end of file
diff --git a/doc/flux_fixpoint/big_int/struct.BigInt.html b/doc/flux_fixpoint/big_int/struct.BigInt.html
index 1e1d0a0fce..19f28795df 100644
--- a/doc/flux_fixpoint/big_int/struct.BigInt.html
+++ b/doc/flux_fixpoint/big_int/struct.BigInt.html
@@ -1,4 +1,4 @@
-BigInt in flux_fixpoint::big_int - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/constant.NAME0.html b/doc/flux_fixpoint/constraint/constant.NAME0.html
deleted file mode 100644
index 197654487b..0000000000
--- a/doc/flux_fixpoint/constraint/constant.NAME0.html
+++ /dev/null
@@ -1 +0,0 @@
-NAME0 in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/constant.NAME1.html b/doc/flux_fixpoint/constraint/constant.NAME1.html
deleted file mode 100644
index 909c9c6a36..0000000000
--- a/doc/flux_fixpoint/constraint/constant.NAME1.html
+++ /dev/null
@@ -1 +0,0 @@
-NAME1 in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/constant.NAME2.html b/doc/flux_fixpoint/constraint/constant.NAME2.html
deleted file mode 100644
index 7ff74adc9e..0000000000
--- a/doc/flux_fixpoint/constraint/constant.NAME2.html
+++ /dev/null
@@ -1 +0,0 @@
-NAME2 in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.BinOp.html b/doc/flux_fixpoint/constraint/enum.BinOp.html
index d44f79857a..c28eeb4ac3 100644
--- a/doc/flux_fixpoint/constraint/enum.BinOp.html
+++ b/doc/flux_fixpoint/constraint/enum.BinOp.html
@@ -1,4 +1,4 @@
-BinOp in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Constant.html b/doc/flux_fixpoint/constraint/enum.Constant.html
index d6e8bbf702..337f1309cc 100644
--- a/doc/flux_fixpoint/constraint/enum.Constant.html
+++ b/doc/flux_fixpoint/constraint/enum.Constant.html
@@ -1,15 +1,15 @@
-Constant in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Constraint.html b/doc/flux_fixpoint/constraint/enum.Constraint.html
index 23fee2100a..7238be3b79 100644
--- a/doc/flux_fixpoint/constraint/enum.Constraint.html
+++ b/doc/flux_fixpoint/constraint/enum.Constraint.html
@@ -1,19 +1,28 @@
-Constraint in flux_fixpoint::constraint - Rust
Returns true if the constraint has at least one concrete RHS (“head”) predicates.
+ Guard(Pred<T>, Box<Self>),
+ ForAll(T::Var, Sort, Pred<T>, Box<Self>),
+}
Returns true if the constraint has at least one concrete RHS (“head”) predicates.
If !c.is_concrete then c is trivially satisfiable and we can avoid calling fixpoint.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Expr.html b/doc/flux_fixpoint/constraint/enum.Expr.html
index 5b50f4cf12..a4192ab79a 100644
--- a/doc/flux_fixpoint/constraint/enum.Expr.html
+++ b/doc/flux_fixpoint/constraint/enum.Expr.html
@@ -1,20 +1,24 @@
-Expr in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Func.html b/doc/flux_fixpoint/constraint/enum.Func.html
index 8484a9d2c4..8e27cf6d60 100644
--- a/doc/flux_fixpoint/constraint/enum.Func.html
+++ b/doc/flux_fixpoint/constraint/enum.Func.html
@@ -1,12 +1,15 @@
-Func in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Pred.html b/doc/flux_fixpoint/constraint/enum.Pred.html
index 9e1872753f..c0613ce3ba 100644
--- a/doc/flux_fixpoint/constraint/enum.Pred.html
+++ b/doc/flux_fixpoint/constraint/enum.Pred.html
@@ -1,10 +1,20 @@
-Pred in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.Proj.html b/doc/flux_fixpoint/constraint/enum.Proj.html
index 246604ef68..0e2a279629 100644
--- a/doc/flux_fixpoint/constraint/enum.Proj.html
+++ b/doc/flux_fixpoint/constraint/enum.Proj.html
@@ -1,9 +1,9 @@
-Proj in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.SortCtor.html b/doc/flux_fixpoint/constraint/enum.SortCtor.html
index a2cb19cf56..e5ba184ab4 100644
--- a/doc/flux_fixpoint/constraint/enum.SortCtor.html
+++ b/doc/flux_fixpoint/constraint/enum.SortCtor.html
@@ -1,7 +1,7 @@
-SortCtor in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/enum.UnOp.html b/doc/flux_fixpoint/constraint/enum.UnOp.html
index 4ae89c340e..74ba320670 100644
--- a/doc/flux_fixpoint/constraint/enum.UnOp.html
+++ b/doc/flux_fixpoint/constraint/enum.UnOp.html
@@ -1,11 +1,11 @@
-UnOp in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/index.html b/doc/flux_fixpoint/constraint/index.html
index cb84883cea..98833e56ac 100644
--- a/doc/flux_fixpoint/constraint/index.html
+++ b/doc/flux_fixpoint/constraint/index.html
@@ -1 +1 @@
-flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/sidebar-items.js b/doc/flux_fixpoint/constraint/sidebar-items.js
index 23a8ce6cc8..76279f46f1 100644
--- a/doc/flux_fixpoint/constraint/sidebar-items.js
+++ b/doc/flux_fixpoint/constraint/sidebar-items.js
@@ -1 +1 @@
-window.SIDEBAR_ITEMS = {"constant":["NAME0","NAME1","NAME2"],"enum":["BinOp","Constant","Constraint","Expr","Func","Pred","Proj","Sort","SortCtor","UnOp"],"static":["DEFAULT_QUALIFIERS"],"struct":["Const","ConstName","FmtParens","FuncSort","KVid","Name","PolyFuncSort","PredTag","Qualifier"]};
\ No newline at end of file
+window.SIDEBAR_ITEMS = {"enum":["BinOp","Constant","Constraint","Expr","Func","Pred","Proj","Sort","SortCtor","UnOp"],"static":["DEFAULT_QUALIFIERS"],"struct":["Const","FmtParens","FuncSort","PolyFuncSort","PredTag","Qualifier"]};
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/static.DEFAULT_QUALIFIERS.html b/doc/flux_fixpoint/constraint/static.DEFAULT_QUALIFIERS.html
index 7663199483..dd446ac52f 100644
--- a/doc/flux_fixpoint/constraint/static.DEFAULT_QUALIFIERS.html
+++ b/doc/flux_fixpoint/constraint/static.DEFAULT_QUALIFIERS.html
@@ -1 +1 @@
-DEFAULT_QUALIFIERS in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.Const.html b/doc/flux_fixpoint/constraint/struct.Const.html
index 7acf52c2c0..6712f7d177 100644
--- a/doc/flux_fixpoint/constraint/struct.Const.html
+++ b/doc/flux_fixpoint/constraint/struct.Const.html
@@ -1,7 +1,14 @@
-Const in flux_fixpoint::constraint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.FmtParens.html b/doc/flux_fixpoint/constraint/struct.FmtParens.html
index dbc83364d2..7d7c24927e 100644
--- a/doc/flux_fixpoint/constraint/struct.FmtParens.html
+++ b/doc/flux_fixpoint/constraint/struct.FmtParens.html
@@ -1,4 +1,8 @@
-FmtParens in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.KVid.html b/doc/flux_fixpoint/constraint/struct.KVid.html
deleted file mode 100644
index 7205443935..0000000000
--- a/doc/flux_fixpoint/constraint/struct.KVid.html
+++ /dev/null
@@ -1,51 +0,0 @@
-KVid in flux_fixpoint::constraint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.Name.html b/doc/flux_fixpoint/constraint/struct.Name.html
deleted file mode 100644
index 958e0db68f..0000000000
--- a/doc/flux_fixpoint/constraint/struct.Name.html
+++ /dev/null
@@ -1,51 +0,0 @@
-Name in flux_fixpoint::constraint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.PolyFuncSort.html b/doc/flux_fixpoint/constraint/struct.PolyFuncSort.html
index 856603055e..f4dd9d61e0 100644
--- a/doc/flux_fixpoint/constraint/struct.PolyFuncSort.html
+++ b/doc/flux_fixpoint/constraint/struct.PolyFuncSort.html
@@ -1,11 +1,11 @@
-PolyFuncSort in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/constraint/struct.PredTag.html b/doc/flux_fixpoint/constraint/struct.PredTag.html
index 741e364e12..763c713775 100644
--- a/doc/flux_fixpoint/constraint/struct.PredTag.html
+++ b/doc/flux_fixpoint/constraint/struct.PredTag.html
@@ -1,9 +1,16 @@
-PredTag in flux_fixpoint::constraint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.BinOp.html b/doc/flux_fixpoint/enum.BinOp.html
index e01384463b..d6b96f7582 100644
--- a/doc/flux_fixpoint/enum.BinOp.html
+++ b/doc/flux_fixpoint/enum.BinOp.html
@@ -1,4 +1,4 @@
-BinOp in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.Constant.html b/doc/flux_fixpoint/enum.Constant.html
index ebf0652291..18dd6d60ff 100644
--- a/doc/flux_fixpoint/enum.Constant.html
+++ b/doc/flux_fixpoint/enum.Constant.html
@@ -1,15 +1,15 @@
-Constant in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.Constraint.html b/doc/flux_fixpoint/enum.Constraint.html
index 8dd2631e68..ad250d8a44 100644
--- a/doc/flux_fixpoint/enum.Constraint.html
+++ b/doc/flux_fixpoint/enum.Constraint.html
@@ -1,19 +1,28 @@
-Constraint in flux_fixpoint - Rust
Returns true if the constraint has at least one concrete RHS (“head”) predicates.
+ Guard(Pred<T>, Box<Self>),
+ ForAll(T::Var, Sort, Pred<T>, Box<Self>),
+}
Returns true if the constraint has at least one concrete RHS (“head”) predicates.
If !c.is_concrete then c is trivially satisfiable and we can avoid calling fixpoint.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.Expr.html b/doc/flux_fixpoint/enum.Expr.html
index c909b26a9f..04cb8bf37b 100644
--- a/doc/flux_fixpoint/enum.Expr.html
+++ b/doc/flux_fixpoint/enum.Expr.html
@@ -1,20 +1,24 @@
-Expr in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.FixpointResult.html b/doc/flux_fixpoint/enum.FixpointResult.html
index a9754224aa..67da4daefb 100644
--- a/doc/flux_fixpoint/enum.FixpointResult.html
+++ b/doc/flux_fixpoint/enum.FixpointResult.html
@@ -1,9 +1,9 @@
-FixpointResult in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.Pred.html b/doc/flux_fixpoint/enum.Pred.html
index f67e4855bd..15d9ef7957 100644
--- a/doc/flux_fixpoint/enum.Pred.html
+++ b/doc/flux_fixpoint/enum.Pred.html
@@ -1,10 +1,20 @@
-Pred in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.Proj.html b/doc/flux_fixpoint/enum.Proj.html
index 9a866e9c6a..26026ed5c8 100644
--- a/doc/flux_fixpoint/enum.Proj.html
+++ b/doc/flux_fixpoint/enum.Proj.html
@@ -1,9 +1,9 @@
-Proj in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.SortCtor.html b/doc/flux_fixpoint/enum.SortCtor.html
index f2c56abc54..083ea43c98 100644
--- a/doc/flux_fixpoint/enum.SortCtor.html
+++ b/doc/flux_fixpoint/enum.SortCtor.html
@@ -1,7 +1,7 @@
-SortCtor in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/enum.UnOp.html b/doc/flux_fixpoint/enum.UnOp.html
index f5421aa5b4..6cb479a747 100644
--- a/doc/flux_fixpoint/enum.UnOp.html
+++ b/doc/flux_fixpoint/enum.UnOp.html
@@ -1,11 +1,11 @@
-UnOp in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/index.html b/doc/flux_fixpoint/index.html
index 787de5b9b1..46a70c67c9 100644
--- a/doc/flux_fixpoint/index.html
+++ b/doc/flux_fixpoint/index.html
@@ -1,2 +1,2 @@
flux_fixpoint - Rust
+
+
+
\ No newline at end of file
diff --git a/doc/flux_fixpoint/macro.declare_types.html b/doc/flux_fixpoint/macro.declare_types.html
new file mode 100644
index 0000000000..1107aa07b3
--- /dev/null
+++ b/doc/flux_fixpoint/macro.declare_types.html
@@ -0,0 +1,3 @@
+declare_types in flux_fixpoint - Rust
macro_rules! declare_types {
+ (type KVar = $kvar:ty; type Var = $var:ty; type Tag = $tag:ty;) => { ... };
+}
\ No newline at end of file
diff --git a/doc/flux_fixpoint/sidebar-items.js b/doc/flux_fixpoint/sidebar-items.js
index 7f63040aa6..bcdb55e9a7 100644
--- a/doc/flux_fixpoint/sidebar-items.js
+++ b/doc/flux_fixpoint/sidebar-items.js
@@ -1 +1 @@
-window.SIDEBAR_ITEMS = {"enum":["BinOp","Constant","Constraint","Expr","FixpointResult","Func","Pred","Proj","Sort","SortCtor","UnOp"],"mod":["big_int","constraint"],"struct":["Const","ConstInfo","ConstName","CrashInfo","Error","FuncSort","KVar","KVid","Name","PolyFuncSort","Qualifier","Stats","Task"]};
\ No newline at end of file
+window.SIDEBAR_ITEMS = {"enum":["BinOp","Constant","Constraint","Expr","FixpointResult","Func","Pred","Proj","Sort","SortCtor","UnOp"],"macro":["declare_types"],"mod":["big_int","constraint"],"struct":["Const","ConstInfo","CrashInfo","Error","FuncSort","KVar","PolyFuncSort","Qualifier","Stats","StringTypes","Task"],"trait":["Symbol","Types"]};
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.Const.html b/doc/flux_fixpoint/struct.Const.html
index 3155b1e0d6..91f07b953c 100644
--- a/doc/flux_fixpoint/struct.Const.html
+++ b/doc/flux_fixpoint/struct.Const.html
@@ -1,7 +1,14 @@
-Const in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.ConstName.html b/doc/flux_fixpoint/struct.ConstName.html
deleted file mode 100644
index 641061b723..0000000000
--- a/doc/flux_fixpoint/struct.ConstName.html
+++ /dev/null
@@ -1,51 +0,0 @@
-ConstName in flux_fixpoint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.CrashInfo.html b/doc/flux_fixpoint/struct.CrashInfo.html
index 6e3128ee28..cf5b548519 100644
--- a/doc/flux_fixpoint/struct.CrashInfo.html
+++ b/doc/flux_fixpoint/struct.CrashInfo.html
@@ -1,4 +1,4 @@
-CrashInfo in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.KVar.html b/doc/flux_fixpoint/struct.KVar.html
index 7903f3f95d..9912bfca66 100644
--- a/doc/flux_fixpoint/struct.KVar.html
+++ b/doc/flux_fixpoint/struct.KVar.html
@@ -1,10 +1,15 @@
-KVar in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.KVid.html b/doc/flux_fixpoint/struct.KVid.html
deleted file mode 100644
index ce2cb9dc60..0000000000
--- a/doc/flux_fixpoint/struct.KVid.html
+++ /dev/null
@@ -1,51 +0,0 @@
-KVid in flux_fixpoint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.Name.html b/doc/flux_fixpoint/struct.Name.html
deleted file mode 100644
index e9b690dc6b..0000000000
--- a/doc/flux_fixpoint/struct.Name.html
+++ /dev/null
@@ -1,51 +0,0 @@
-Name in flux_fixpoint - Rust
The provided value must be less than or equal to the maximum value for the newtype.
-Providing a value outside this range is undefined due to layout restrictions.
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.PolyFuncSort.html b/doc/flux_fixpoint/struct.PolyFuncSort.html
index c72aba8a77..52f5c4ea0d 100644
--- a/doc/flux_fixpoint/struct.PolyFuncSort.html
+++ b/doc/flux_fixpoint/struct.PolyFuncSort.html
@@ -1,11 +1,11 @@
-PolyFuncSort in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.Qualifier.html b/doc/flux_fixpoint/struct.Qualifier.html
index 79473321a1..d4e8bce7d8 100644
--- a/doc/flux_fixpoint/struct.Qualifier.html
+++ b/doc/flux_fixpoint/struct.Qualifier.html
@@ -1,11 +1,16 @@
-Qualifier in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.Stats.html b/doc/flux_fixpoint/struct.Stats.html
index 5899e15ece..fe5460a679 100644
--- a/doc/flux_fixpoint/struct.Stats.html
+++ b/doc/flux_fixpoint/struct.Stats.html
@@ -1,9 +1,9 @@
-Stats in flux_fixpoint - Rust
\ No newline at end of file
diff --git a/doc/flux_fixpoint/struct.Task.html b/doc/flux_fixpoint/struct.Task.html
index 8e3162ad9b..1f1898404f 100644
--- a/doc/flux_fixpoint/struct.Task.html
+++ b/doc/flux_fixpoint/struct.Task.html
@@ -1,31 +1,41 @@
-Task in flux_fixpoint - Rust