summaryrefslogtreecommitdiff
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /parsing/g_vernac.ml4
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml438
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: