From a07cc19ddd3759f3cc3c60e2321d62dfb5822b62 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Aug 2014 20:00:59 +0200
Subject: [PATCH] New syntax for types in frontend.

This allows for constant expressions in array sizes and makes way for
future extensions.
---
 theories/option.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/option.v b/theories/option.v
index 78855bef..eba41dd4 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -22,7 +22,6 @@ Proof. congruence. Qed.
 (** The non dependent elimination principle on the option type. *)
 Definition default {A B} (b : B) (x : option A) (f : A → B)  : B :=
   match x with None => b | Some a => f a end.
-Hint Extern 1000 => simpl (default _ (Some _) _) || simpl (default _ None _).
 
 (** The [from_option] function allows us to get the value out of the option
 type by specifying a default value. *)
-- 
GitLab