From 4a66d0d70b6f8fb34598b154b62cde3199bd7101 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 Aug 2018 14:30:35 -0400 Subject: Add eq_ident_Decidable --- src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Experiments') diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v index 4261617af..1e64a1697 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Option. +Require Import Crypto.Util.Decidable. Require Import Crypto.Experiments.NewPipeline.Language. Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypes. @@ -70,6 +71,8 @@ Module Compilers. destruct idc1; reflexivity. } { destruct idc1, idc2; try reflexivity; solve [ inversion pf ]. } Qed. + + Global Instance eq_ident_Decidable : DecidableRel (@eq pattern.ident) := pattern.ident.ident_eq_dec. End ident. End pattern. End Compilers. -- cgit v1.2.3