diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9a98df80..6a9388b2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4 9562 2007-01-31 09:00:36Z msozeau $ *) +(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -202,7 +202,7 @@ GEXTEND Gram def_body: [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -264,8 +264,8 @@ GEXTEND Gram ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) - | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) + | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; @@ -304,7 +304,7 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) | id = name; ":="; b = lconstr -> match b with - CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t)) + CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; assum_list: |