From d52641d2cda2af132c13dcb481f753d51e7af216 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 2010 19:24:43 +0000
Subject: Don't interpret VMcast as an ordinary type cast in Definition a := t
 <: T.

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cc03acf550..f23b835e19 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -241,7 +241,7 @@ GEXTEND Gram
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
       (match c with
-          CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
+          CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
 	DefineBody (bl, red, c, Some t)
-- 
cgit v1.2.3