Imported Upstream version 8.5~beta3+dfsg

7 files changed, 154 insertions, 385 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3bb029a8..e2e6795f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,12 +153,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
-      | id = ident -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
+      | id = identref -> [id]
       ] ]
   ;
   lconstr:
@@ -223,26 +223,29 @@ GEXTEND Gram
           CHole (!@loc, None, IntroAnonymous, Some arg)
       ] ]
   ;
-  forall:
-    [ [ "forall" -> () ] ]
-  ;
-  lambda:
-    [ [ "fun" -> () ] ]
-  ;
   record_declaration:
-    [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
+    [ [ fs = record_fields -> CRecord (!@loc, None, fs)
 (*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
 (* 	  CRecord (!@loc, Some c, fs) *)
     ] ]
   ;
+
+  record_fields:
+    [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
+      | f = record_field_declaration; ";" -> [f]
+      | f = record_field_declaration -> [f]
+      | -> []
+    ] ]
+  ;
+
   record_field_declaration:
     [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
       (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
-    [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+    [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
           mkCProdN (!@loc) bl c
-      | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+      | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
           mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
@@ -308,7 +311,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = ident -> GType (Some (Id.to_string id))
+      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
       ] ]
   ;
   fix_constr:
@@ -362,18 +365,25 @@ GEXTEND Gram
     [ [ pll = LIST1 mult_pattern SEP "|";
         "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
   ;
-  recordpattern:
+  record_pattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
   ;
+  record_patterns:
+    [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
+      | p = record_pattern; ";" -> [p]
+      | p = record_pattern-> [p]
+      | -> []
+    ] ]
+  ;
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
     | "99" RIGHTA [ ]
-    | "10" LEFTA
+    | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
 	  CPatAlias (!@loc, p, id) ]
-    | "9" RIGHTA
+    | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
@@ -388,7 +398,7 @@ GEXTEND Gram
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
       [ r = Prim.reference -> CPatAtom (!@loc,Some r)
-      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+      | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
       | "_" -> CPatAtom (!@loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16..017f0ea5 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
-        l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
-          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = tactic -> ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -73,8 +73,10 @@ GEXTEND Gram
       | IDENT "Unfocused" -> VernacUnfocused
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
+      | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
+      | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
       | IDENT "Show"; IDENT "Goal"; n = string ->
-          VernacShow (ShowGoal (GoalId n))
+          VernacShow (ShowGoal (GoalUid n))
       | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
 	  VernacShow (ShowGoalImplicitly n)
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 69593f99..c94ac846 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -339,21 +339,6 @@ GEXTEND Gram
       | d = delta_flag -> all_with d
     ] ]
   ;
-  red_tactic:
-    [ [ IDENT "red" -> Red false
-      | IDENT "hnf" -> Hnf
-      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
-      | IDENT "cbv"; s = strategy_flag -> Cbv s
-      | IDENT "cbn"; s = strategy_flag -> Cbn s
-      | IDENT "lazy"; s = strategy_flag -> Lazy s
-      | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
-      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
-      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
-      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
-      | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
-  ;
-  (* This is [red_tactic] including possible extensions *)
   red_expr:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
@@ -452,16 +437,6 @@ GEXTEND Gram
     [ [ "using"; l = LIST1 constr SEP "," -> l
       | -> [] ] ]
   ;
-  trivial:
-    [ [ IDENT "trivial" -> Off
-      | IDENT "info_trivial" -> Info
-      | IDENT "debug"; IDENT "trivial" -> Debug ] ]
-  ;
-  auto:
-    [ [ IDENT "auto" -> Off
-      | IDENT "info_auto" -> Info
-      | IDENT "debug"; IDENT "auto" -> Debug ] ]
-  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -627,9 +602,18 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Automation tactic *)
-      | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
-      | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (d,n,lems,db))
+      | IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Off, lems, db))
+      | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Info, lems, db))
+      | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Debug, lems, db))
+      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Off, n, lems, db))
+      | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Info, n, lems, db))
+      | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Debug, n, lems, db))
 
       (* Context management *)
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
@@ -677,7 +661,31 @@ GEXTEND Gram
 	    TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
 
       (* Conversion *)
-      | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
+      | IDENT "red"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Red false, cl))
+      | IDENT "hnf"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Hnf, cl))
+      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+      | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv s, cl))
+      | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbn s, cl))
+      | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Lazy s, cl))
+      | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvVm po, cl))
+      | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvNative po, cl))
+      | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Unfold ul, cl))
+      | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Fold l, cl))
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
 	  let p,cl = merge_occurrences (!@loc) cl oc in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cf7f6af2..1f9f57f6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
 let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
 let command_entry = ref noedit_mode
 let set_command_entry e = command_entry := e
@@ -71,6 +71,17 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -79,6 +90,7 @@ GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; l = vernac_list -> VernacTime l
+      | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
@@ -95,12 +107,12 @@ GEXTEND Gram
       | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
       | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
 
-      | v = vernac_poly -> v ] 
+      | v = vernac_poly -> v ]
     ]
   ;
-  vernac_poly: 
+  vernac_poly:
     [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v)
-      | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) 
+      | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
       | v = vernac_aux -> v ]
     ]
   ;
@@ -128,7 +140,7 @@ GEXTEND Gram
 
   selector:
     [ [ n=natural; ":" -> SelectNth n
-      | "["; id = ident; "]"; ":" -> SelectId id
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
       | IDENT "all" ; ":" -> SelectAll
       | IDENT "par" ; ":" -> SelectAllParallel ] ]
   ;
@@ -145,7 +157,7 @@ GEXTEND Gram
     ] ]
   ;
 
-  subgoal_command: 
+  subgoal_command:
     [ [ c = query_command; "." ->
                   begin function
                     | Some (SelectNth g) -> c (Some g)
@@ -184,9 +196,9 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
+    [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
-          [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
+          [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
           (Some id,(bl,c,None)) ] ->
           VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
@@ -194,10 +206,10 @@ GEXTEND Gram
       | stre = assumptions_token; nl = inline; bl = assum_list ->
 	  test_plurial_form bl;
 	  VernacAssumption (stre, nl, bl)
-      | d = def_token; id = identref; b = def_body ->
+      | d = def_token; id = pidentref; b = def_body ->
           VernacDefinition (d, id, b)
       | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((Some Discharge, Definition), id, b)
+          VernacDefinition ((Some Discharge, Definition), (id, None), b)
       (* Gallina inductive declarations *)
       | priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -248,13 +260,17 @@ GEXTEND Gram
     [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
       | IDENT "Variables" -> (Some Discharge, Definitional)
       | IDENT "Axioms" -> (None, Logical)
-      | IDENT "Parameters" -> (None, Definitional) ] ]
+      | IDENT "Parameters" -> (None, Definitional)
+      | IDENT "Conjectures" -> (None, Conjectural) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
       | IDENT "Inline" -> DefaultInline
       | -> NoInline] ]
   ;
+  pidentref:
+    [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
+  ;
   univ_constraint:
     [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
 	r = identref -> (l, ord, r) ] ]
@@ -299,7 +315,7 @@ GEXTEND Gram
       | -> RecordDecl (None, []) ] ]
   ;
   inductive_definition:
-    [ [ oc = opt_coercion; id = identref; indpar = binders;
+    [ [ oc = opt_coercion; id = pidentref; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
         lc=opt_constructors_or_fields; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
@@ -309,9 +325,9 @@ GEXTEND Gram
       | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
 	  Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
-      | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+      | cstr = identref; "{"; fs = record_fields; "}" ->
 	  RecordDecl (Some cstr,fs)
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+      | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
       |  -> Constructors [] ] ]
   ;
 (*
@@ -325,14 +341,14 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = identref;
+    [ [ id = pidentref;
 	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; ty = type_cstr;
+    [ [ id = pidentref; bl = binders; ty = type_cstr;
         def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -373,6 +389,13 @@ GEXTEND Gram
   [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
       ntn = decl_notation -> (bd,pri),ntn ] ]
   ;
+  record_fields:
+    [ [ f = record_field; ";"; fs = record_fields -> f :: fs
+      | f = record_field; ";" -> [f]
+      | f = record_field -> [f]
+      | -> []
+    ] ]
+  ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
          t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
@@ -397,7 +420,7 @@ GEXTEND Gram
     [ [ "("; a = simple_assum_coe; ")" -> a ] ]
   ;
   simple_assum_coe:
-    [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
+    [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
         (not (Option.is_empty oc),(idl,c)) ] ]
   ;
 
@@ -424,20 +447,24 @@ GEXTEND Gram
   ;
 END
 
-let only_identrefs =
-  Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+  Gram.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
       match get_tok (Util.stream_nth n strm) with
         | KEYWORD "." -> ()
         | KEYWORD ")" -> ()
-        | IDENT _ -> aux (n+1)
+        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
         | _ -> raise Stream.Failure in
       aux 0)
+let starredidentreflist_to_expr l =
+  match l with
+  | [] -> SsEmpty
+  | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
 (* Modules and Sections *)
 GEXTEND Gram
-  GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+  GLOBAL: gallina_ext module_expr module_type section_subset_expr;
 
   gallina_ext:
     [ [ (* Interactive module declaration *)
@@ -460,7 +487,7 @@ GEXTEND Gram
       | IDENT "End"; id = identref -> VernacEndSegment id
 
       (* Naming a set of section hyps *)
-      | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
           VernacNameSectionHypSet (id, expr)
 
       (* Requiring an already compiled module *)
@@ -551,22 +578,32 @@ GEXTEND Gram
           CMwith (!@loc,mty,decl)
       ] ]
   ;
-  section_subset_descr:
-    [ [ IDENT "All" -> SsAll
-      | "Type" -> SsType
-      | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
-      | e = section_subset_expr -> SsExpr e ] ]
-  ;
+  (* Proof using *)
   section_subset_expr:
+    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+          starredidentreflist_to_expr l
+      | e = ssexpr -> e ]]
+  ;
+  starredidentref:
+    [ [ i = identref -> SsSingl i
+      | i = identref; "*" -> SsFwdClose(SsSingl i)
+      | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+      | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+  ;
+  ssexpr:
     [ "35" 
-      [ "-"; e = section_subset_expr -> SsCompl e ]
+      [ "-"; e = ssexpr -> SsCompl e ]
     | "50"
-      [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
-      | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+      [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+      | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
     | "0"
-      [ i = identref -> SsSet [i]
-      | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
-      | "("; e = section_subset_expr; ")"-> e ] ]
+      [ i = starredidentref -> i
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+          starredidentreflist_to_expr l
+      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+          SsFwdClose(starredidentreflist_to_expr l)
+      | "("; e = ssexpr; ")"-> e 
+      | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
   ;
 END
 
@@ -592,15 +629,15 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
+	    ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (true, f, s, t)
@@ -1041,7 +1078,9 @@ GEXTEND Gram
          VernacOpenCloseScope (local,(false,sc))
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
-	 VernacDelimiters (sc,key)
+	 VernacDelimiters (sc, Some key)
+     | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
+	 VernacDelimiters (sc, None)
 
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
        refl = LIST1 smart_global -> VernacBindScope (sc,refl)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
deleted file mode 100644
index 84e4a573..00000000
--- a/parsing/g_xml.ml4
+++ /dev/null
@@ -1,290 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Compat
-open Pp
-open Errors
-open Util
-open Names
-open Pcoq
-open Glob_term
-open Tacexpr
-open Libnames
-open Globnames
-open Detyping
-open Misctypes
-open Decl_kinds
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-(* Generic xml parser without raw data *)
-
-type attribute = string * (Loc.t * string)
-type xml = XmlTag of Loc.t * string * attribute list * xml list
-
-let check_tags loc otag ctag =
-  if not (String.equal otag ctag) then
-    user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
-      str "does not match open xml tag " ++ str otag ++ str ".")
-
-let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
-
-GEXTEND Gram
-  GLOBAL: xml_eoi;
-
-  xml_eoi:
-    [ [ x = xml; EOI -> x ] ]
-  ;
-  xml:
-    [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
-        "<"; "/"; ctag = IDENT; ">"  ->
-	  check_tags (!@loc) otag ctag;
-	  XmlTag (!@loc,ctag,attrs,l)
-      | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
-	  XmlTag (!@loc,tag,attrs,[])
-    ] ]
-  ;
-  attr:
-    [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
-  ;
-END
-
-(* Errors *)
-
-let error_bad_arity loc n =
-  let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
-  user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^")."))
-
-(* Interpreting attributes *)
-
-let nmtoken (loc,a) =
-  try int_of_string a
-  with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-
-let get_xml_attr s al =
-  try String.List.assoc s al
-  with Not_found -> error ("No attribute "^s)
-
-(* Interpreting specific attributes *)
-
-let ident_of_cdata (loc,a) = Id.of_string a
-
-let uri_of_data s =
-  try
-    let n = String.index s ':' in
-    let p = String.index s '.' in
-    let s = String.sub s (n+2) (p-n-2) in
-    for i = 0 to String.length s - 1 do
-      match s.[i] with
-      | '/' -> s.[i] <- '.'
-      | _ -> ()
-    done;
-    qualid_of_string s
-  with Not_found | Invalid_argument _ ->
-    error ("Malformed URI \""^s^"\"")
-
-let constant_of_cdata (loc,a) =
-  let q = uri_of_data a in
-  try Nametab.locate_constant q
-  with Not_found -> error ("No such constant "^string_of_qualid q)
-
-let global_of_cdata (loc,a) =
-  let q = uri_of_data a in
-  try Nametab.locate q
-  with Not_found -> error ("No such global "^string_of_qualid q)
-
-let inductive_of_cdata a = match global_of_cdata a with
-  | IndRef (kn,_) -> kn
-  | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive")
-
-let ltacref_of_cdata (loc,a) =
-  let q = uri_of_data a in
-  try (loc,Nametab.locate_tactic q)
-  with Not_found -> error ("No such ltac "^string_of_qualid q)
-
-let sort_of_cdata (loc,a) = match a with
-  | "Prop" -> GProp
-  | "Set" -> GSet
-  | "Type" -> GType None
-  | _ -> user_err_loc (loc,"",str "sort expected.")
-
-let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
-
-let get_xml_inductive_kn al =
-  inductive_of_cdata (* uriType apparent synonym of uri *)
-    (try get_xml_attr "uri" al
-     with UserError _ -> get_xml_attr "uriType" al)
-
-let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
-
-let get_xml_inductive al =
-  (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al))
-
-let get_xml_constructor al =
-  (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-
-let get_xml_binder al =
-  try Name (ident_of_cdata (String.List.assoc "binder" al))
-  with Not_found -> Anonymous
-
-let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
-
-let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
-
-let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
-
-let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al))
-
-(* A leak in the xml dtd: arities of constructor need to know global env *)
-
-let compute_branches_lengths ind =
-  let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
-  mip.Declarations.mind_consnrealdecls
-
-let compute_inductive_ndecls ind =
-  Inductiveops.inductive_nrealdecls ind
-
-(* Interpreting constr as a glob_constr *)
-
-let rec interp_xml_constr = function
-  | XmlTag (loc,"REL",al,[]) ->
-      GVar (loc, get_xml_ident al)
-  | XmlTag (loc,"VAR",al,[]) ->
-      error "XML parser: unable to interp free variables"
-  | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
-      let body,decls = List.sep_last xl in
-      let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
-	ctx (interp_xml_target body)
-  | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
-      let body,decls = List.sep_last xl in
-      let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
-	ctx (interp_xml_target body)
-  | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
-      let body,defs = List.sep_last xl in
-      let ctx = List.map interp_xml_def defs in
-      List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
-        ctx (interp_xml_target body)
-  | XmlTag (loc,"APPLY",_,x::xl) ->
-      GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
-  | XmlTag (loc,"instantiate",_,
-      (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
-      GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
-  | XmlTag (loc,"META",al,xl) ->
-      GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl))
-  | XmlTag (loc,"CONST",al,[]) ->
-      GRef (loc, ConstRef (get_xml_constant al), None)
-  | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
-      let ind = get_xml_inductive al in
-      let p = interp_xml_patternsType x in
-      let tm = interp_xml_inductiveTerm y in
-      let vars = compute_branches_lengths ind in
-      let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
-      in
-      let mat = simple_cases_matrix_of_branches ind brs in
-      let n = compute_inductive_ndecls ind in
-      let nal,rtn = return_type_of_predicate ind n p in
-      GCases (loc,RegularStyle,rtn,[tm,nal],mat)
-  | XmlTag (loc,"MUTIND",al,[]) ->
-      GRef (loc, IndRef (get_xml_inductive al), None)
-  | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
-      GRef (loc, ConstructRef (get_xml_constructor al), None)
-  | XmlTag (loc,"FIX",al,xl) ->
-      let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
-      let ln,lc,lt = List.split3 lnct in
-      let lctx = List.map (fun _ -> []) ln in
-      GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
-  | XmlTag (loc,"COFIX",al,xl) ->
-      let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
-      GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
-  | XmlTag (loc,"CAST",al,[x1;x2]) ->
-      GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
-  | XmlTag (loc,"SORT",al,[]) ->
-      GSort (loc, get_xml_sort al)
-  | XmlTag (loc,s,_,_) ->
-      user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-and interp_xml_tag s = function
-  | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
-  | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
-    str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
-
-and interp_xml_constr_alias s x =
-  match interp_xml_tag s x with
-    | (_,_,[x]) -> interp_xml_constr x
-    | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_term x = interp_xml_constr_alias "term" x
-and interp_xml_type x = interp_xml_constr_alias "type" x
-and interp_xml_target x = interp_xml_constr_alias "target" x
-and interp_xml_body x = interp_xml_constr_alias "body" x
-and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
-and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
-and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
-and interp_xml_arg x = interp_xml_constr_alias "arg" x
-and interp_xml_substitution x =
-  match interp_xml_tag "substitution" x with
-    _, al, [x] -> get_xml_name al, interp_xml_constr x
-  | loc, _, _ -> error_bad_arity loc 1
-                     (* no support for empty substitution from official dtd *)
-
-and interp_xml_decl_alias s x =
-  match interp_xml_tag s x with
-    | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
-    | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_def x = interp_xml_decl_alias "def" x
-and interp_xml_decl x = interp_xml_decl_alias "decl" x
-
-and interp_xml_recursionOrder x =
-  let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
-  let (locs, s) = get_xml_attr "type" al in
-  match s, l with
-  | "Structural", [] -> GStructRec
-  | "Structural", _ -> error_bad_arity loc 0
-  | "WellFounded", [c] -> GWfRec (interp_xml_type c)
-  | "WellFounded", _ -> error_bad_arity loc 1
-  | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
-  | "Measure", _ -> error_bad_arity loc 2
-  | _ -> user_err_loc (locs,"",str "Invalid recursion order.")
-
-and interp_xml_FixFunction x =
-  match interp_xml_tag "FixFunction" x with
-  | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
-      ((Some (nmtoken (get_xml_attr "recIndex" al)),
-	interp_xml_recursionOrder x1),
-       (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
-  | (loc,al,[x1;x2]) ->
-      ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
-       (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
-  | (loc,_,_) ->
-      error_bad_arity loc 1
-
-and interp_xml_CoFixFunction x =
-  match interp_xml_tag "CoFixFunction" x with
-  | (loc,al,[x1;x2]) ->
-      (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
-    | (loc,_,_) ->
-	error_bad_arity loc 1
-
-(* Interpreting tactic argument *)
-
-let rec interp_xml_tactic_arg = function
-  | XmlTag (loc,"TERM",[],[x]) ->
-      ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
-  | XmlTag (loc,"CALL",al,xl) ->
-      let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
-      TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
-  | XmlTag (loc,s,_,_) ->
-      user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-let parse_tactic_arg ch =
-  interp_xml_tactic_arg
-    (Pcoq.Gram.entry_parse xml_eoi
-       (Pcoq.Gram.parsable (Stream.of_channel ch)))
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 8e839296..c6d5f3b9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -70,7 +70,7 @@ let ttree_remove ttree str =
   remove ttree 0
 
 
-(* Errors occuring while lexing (explained as "Lexer error: ...") *)
+(* Errors occurring while lexing (explained as "Lexer error: ...") *)
 
 module Error = struct
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 54edbb2c..2e47e07a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -298,7 +298,7 @@ module Prim =
   struct
     let gec_gen x = make_gen_entry uprim x
 
-    (* Entries that can be refered via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Gram.entry table *)
     (* Typically for tactic or vernac extensions *)
     let preident = gec_gen (rawwit wit_pre_ident) "preident"
     let ident = gec_gen (rawwit wit_ident) "ident"
@@ -334,7 +334,7 @@ module Constr =
   struct
     let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
 
-    (* Entries that can be refered via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Gram.entry table *)
     let constr = gec_constr "constr"
     let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
@@ -367,7 +367,7 @@ module Tactic =
     (* Main entry for extensions *)
     let simple_tactic = Gram.entry_create "tactic:simple_tactic"
 
-    (* Entries that can be refered via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
       make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
@@ -459,8 +459,8 @@ let default_pattern_levels =
   [200,Extend.RightA,true;
    100,Extend.RightA,false;
    99,Extend.RightA,true;
-   10,Extend.LeftA,false;
-   9,Extend.RightA,false;
+   11,Extend.LeftA,false;
+   10,Extend.RightA,false;
    1,Extend.LeftA,false;
    0,Extend.RightA,false]