From 3f768f404a36ebd3e2a5b10a9fe48e5122e4cd62 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 10 Apr 2016 18:14:09 +0200
Subject: Adding option "Set Reversible Pattern Implicit" to Specif.v so that
 an implicit is found whether one writes (sig P) or {x|P x}.

---
 theories/Init/Specif.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 6c0221856e..d1038186e3 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -9,6 +9,7 @@
 (** 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