From 4484d5fc42c90bff13a1b9454a93b99b3fb94576 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 24 Nov 2011 10:54:39 +0000
Subject: Correct direction for definitional typeclasses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14722 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 916a305c22..8e370bc734 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -415,7 +415,7 @@ let vernac_inductive finite infer indl =
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
-	let coe' = if coe then Some false else None in
+	let coe' = if coe then Some true else None in
 	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) finite infer id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
-- 
cgit v1.2.3