From 1758dade15ff584949a9e4bd6b21ce1a58e42ff3 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 12 Mar 2011 16:33:14 -0800 Subject: [PATCH] Remove unnecessary coreVar_eq_refl axiom --- src/HaskCoreVars.v | 1 - 1 file changed, 1 deletion(-) diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index 954dfc5..9225974 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -11,7 +11,6 @@ Require Import Coq.Strings.String. Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var". Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)". Variable coreVarToString : CoreVar -> string. Extract Inlined Constant coreVarToString => "outputableToString". -Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }. Instance CoreVarToString : ToString CoreVar := { toString := coreVarToString }. -- 1.7.10.4