aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-06-24 18:28:53 +0100
committerYann Herklotz <git@yannherklotz.com>2022-06-24 18:28:53 +0100
commit56f1dd7a658dd21bb267dc41fc0301adbd620a6d (patch)
tree12f55df14f2e73a7b14f461cee837e79b15cb502 /src
parent0a7f2f6f6e0f68a9fa89a27dc677b40f8dfb6e86 (diff)
downloadvericert-56f1dd7a658dd21bb267dc41fc0301adbd620a6d.tar.gz
vericert-56f1dd7a658dd21bb267dc41fc0301adbd620a6d.zip
Update build files for documentation
Diffstat (limited to 'src')
-rw-r--r--src/hls/Gible.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index 399935b..8971535 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -16,9 +16,9 @@
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
-=============
-RTLBlockInstr
-=============
+=====
+Gible
+=====
These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
consistent instructions, which greatly simplifies the proofs, as they will by