Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

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: