summaryrefslogtreecommitdiff
path: root/parsing/g_proofs.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r--parsing/g_proofs.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2f515a81..0a48748f 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_proofs.ml4 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: g_proofs.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
open Pcoq
open Pp
@@ -118,6 +118,6 @@ GEXTEND Gram
;
constr_body:
[ [ ":="; c = lconstr -> c
- | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ]
+ | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ]
;
END