move brand_eq_dec to where it belongs

querycert · Sep 16, 2020 · c99bce2 · c99bce2
1 parent 15d2783
commit c99bce2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/compiler/core/Brands/BrandRelation.v b/compiler/core/Brands/BrandRelation.v
@@ -32,6 +32,11 @@ Definition any : brands := nil.
 
 Definition brand_relation_t := list (string*string).
 
+Lemma brand_eq_dec : EqDec brand eq.
+Proof.
+  repeat red. apply string_dec.
+Defined.
+
 Section brand_relation_types.
   Context  (brand_relation_brands:brand_relation_t).
 

diff --git a/compiler/core/Data/Model/Data.v b/compiler/core/Data/Model/Data.v
@@ -156,11 +156,6 @@ Section Data.
       intros. apply (H (x,y)). trivial.
   Qed.
 
-  Lemma brand_eq_dec : EqDec brand eq.
-  Proof.
-    repeat red. apply string_dec.
-  Defined.
-
   (** Equality is decidable for data *)
   Lemma data_eq_dec : forall x y:data, {x=y}+{x<>y}.
   Proof.