From 51a7fae33e0056581cb3ab7e7595090cad97878a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 11 Mar 2020 09:40:55 -0400 Subject: [PATCH] Unnecessary Fixpoint --- CompilerCorrectness.v | 2 +- CompilerCorrectness_template.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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