aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--parsing/g_vernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cc03acf55..f23b835e1 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)