diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 38 |
1 files changed, 22 insertions, 16 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c3ea4d22..1f5a6cf9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp @@ -134,9 +134,9 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr; + [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 - [ "with"; id = identref; bl = binders_let; ":"; c = lconstr -> + [ "with"; id = identref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c,None)) ] -> VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook) | stre = assumption_token; nl = inline; bl = assum_list -> @@ -170,7 +170,7 @@ GEXTEND Gram ; gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; - ps = binders_let; + ps = binders; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> @@ -231,13 +231,13 @@ GEXTEND Gram ; (* Simple definitions *) def_body: - [ [ bl = binders_let; ":="; red = reduce; c = lconstr -> + [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) - | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> + | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) - | bl = binders_let; ":"; t = lconstr -> + | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; reduce: @@ -254,7 +254,7 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; oc = opt_coercion; indpar = binders_let; + [ [ id = identref; oc = opt_coercion; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] @@ -281,13 +281,13 @@ GEXTEND Gram (* (co)-fixpoints *) rec_definition: [ [ id = identref; - bl = binders_let_fixannot; + bl = binders_fixannot; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = identref; bl = binders_let; ty = type_cstr; + [ [ id = identref; bl = binders; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -305,6 +305,10 @@ GEXTEND Gram IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + | IDENT "Elimination"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + | IDENT "Case"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) @@ -324,12 +328,12 @@ GEXTEND Gram [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] ; record_binder_body: - [ [ l = binders_let; oc = of_type_with_opt_coercion; + [ [ l = binders; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t)) - | l = binders_let; oc = of_type_with_opt_coercion; + | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> fun id -> (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) - | l = binders_let; ":="; b = lconstr -> fun id -> + | l = binders; ":="; b = lconstr -> fun id -> match b with | CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) @@ -352,7 +356,7 @@ GEXTEND Gram ; constructor_type: - [[ l = binders_let; + [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (coe,(id,mkCProdN loc l c)) | -> @@ -527,7 +531,7 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) - | IDENT "Context"; c = binders_let -> + | IDENT "Context"; c = binders -> VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; @@ -577,7 +581,7 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders_let -> + [ [ name = identref; sup = OPT binders -> (let (loc,id) = name in (loc, Name id)), (Option.default [] sup) | -> (loc, Anonymous), [] ] ] @@ -922,6 +926,8 @@ GEXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint + | IDENT "binder" -> ETBinder true + | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; opt_scope: |