make some fixpoints local

mit-plv · Dec 19, 2024 · f49da82 · f49da82
1 parent 21d12fa
commit f49da82
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/bedrock2/src/bedrock2Examples/ct.v b/bedrock2/src/bedrock2Examples/ct.v
@@ -75,7 +75,7 @@ Definition getline_io n bs :=
   let newline := if n =? length bs then nil else [getchar_event Byte.x0a] in
   newline ++ chars.
 
-Fixpoint getline_leakage f dst n (bs : nat) (i : word) :=
+Local Fixpoint getline_leakage f dst n (bs : nat) (i : word) :=
   if i =? n then leak_bool false :: nil else
   match bs with
   | S bs => getline_leakage f dst n bs (add i (of_Z 1)) ++ (leak_word (add dst i) :: leak_bool false :: f ++ leak_unit :: leak_bool true :: nil)

diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
@@ -55,7 +55,7 @@ Section WithParameters.
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
-  Fixpoint newtrace x y n :=
+  Local Fixpoint newtrace x y n :=
     match n with
     | S n' => newtrace (word.add x (word.of_Z 1)) (word.add y (word.of_Z 1)) n' ++
                [leak_word y; leak_word x; leak_bool true]