diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v
index c571e4b..5622ebb 100644
--- a/CompilerCorrectness.v
+++ b/CompilerCorrectness.v
@@ -901,7 +901,7 @@ Compute tempVar 2.
  * lack of clashes.  We also prove some properties that will come in handy
  * later. *)
 
-Fixpoint noUnderscoreVar (x : var) : bool :=
+Definition noUnderscoreVar (x : var) : bool :=
   match x with
   | String "_" _ => false
   | _ => true
diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v
index dcf571c..4e3e52b 100644
--- a/CompilerCorrectness_template.v
+++ b/CompilerCorrectness_template.v
@@ -613,7 +613,7 @@ Compute tempVar 0.
 Compute tempVar 1.
 Compute tempVar 2.
 
-Fixpoint noUnderscoreVar (x : var) : bool :=
+Definition noUnderscoreVar (x : var) : bool :=
   match x with
   | String "_" _ => false
   | _ => true