From ee374eb0bbf32f192f474be25ad23bd21604d583 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:04 +0200
Subject: Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v
 so that an"

This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
---
 theories/Init/Specif.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1038186e3..6c0221856e 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -9,7 +9,6 @@
 (** Basic specifications : sets that may contain logical information *)
 
 Set Implicit Arguments.
-Set Reversible Pattern Implicit.
 
 Require Import Notations.
 Require Import Datatypes.
-- 
cgit v1.2.3