From 8ee03c1561cd622e98dfa2669cb8e94a53c859c7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Jun 2010 13:45:44 +0000
Subject: MSetInterface: no induction principle about a Record (nicer
 extraction)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13159 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/MSets/MSetInterface.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 7dc3c96a86..6de91daccf 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -429,6 +429,10 @@ End WRawSets.
 
 Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
+ (** We avoid creating induction principles for the Record *)
+ Local Unset Elimination Schemes.
+ Local Unset Case Analysis Schemes.
+
  Definition elt := E.t.
 
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
-- 
cgit v1.2.3