From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: Removing internal support for accepting "{struct x}" and co in
 "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
---
 parsing/g_vernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 71b93439bc..6ede0490e4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -146,8 +146,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
-          (Some id,(bl,c,None)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
+          (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 parsing/cLexer.ml4 | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'parsing')

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 6d259e1b12..f25b394f0b 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -345,13 +345,13 @@ let rec string loc ~comm_level bp len = parser
       if esc then string loc ~comm_level bp (store len '"') s else (loc, len)
   | [< ''('; s >] ->
       (parser
-        | [< ''*'; s >] ->
-            string loc
-              (Option.map succ comm_level)
+      | [< ''*'; s >] ->
+        let comm_level = Option.map succ comm_level in
+            string loc ~comm_level
               bp (store (store len '(') '*')
               s
         | [< >] ->
-            string loc comm_level bp (store len '(') s) s
+            string loc ~comm_level bp (store len '(') s) s
   | [< ''*'; s >] ->
       (parser
         | [< '')'; s >] ->
@@ -361,9 +361,9 @@ let rec string loc ~comm_level bp len = parser
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
-            string loc comm_level bp (store (store len '*') ')') s
+            string loc ~comm_level bp (store (store len '*') ')') s
         | [< >] ->
-            string loc comm_level bp (store len '*') s) s
+            string loc ~comm_level bp (store len '*') s) s
   | [< ''\n' as c; s >] ep ->
      (* If we are parsing a comment, the string if not part of a token so we
      update the first line of the location. Otherwise, we update the last
@@ -372,8 +372,8 @@ let rec string loc ~comm_level bp len = parser
        if Option.has_some comm_level then bump_loc_line loc ep
        else bump_loc_line_last loc ep
      in
-     string loc comm_level bp (store len c) s
-  | [< 'c; s >] -> string loc comm_level bp (store len c) s
+     string loc ~comm_level bp (store len c) s
+  | [< 'c; s >] -> string loc ~comm_level bp (store len c) s
   | [< _ = Stream.empty >] ep ->
      let loc = set_loc_pos loc bp ep in
      err loc Unterminated_string
@@ -613,7 +613,7 @@ let rec next_token loc = parser bp
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
       (INT (get_buff len), set_loc_pos loc bp ep)
-  | [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
+  | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep ->
       comment_stop bp;
       (STRING (get_buff len), set_loc_pos loc bp ep)
   | [< ' ('(' as c);
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 parsing/cLexer.ml4   | 8 --------
 parsing/egramcoq.ml  | 4 ----
 parsing/g_vernac.ml4 | 5 -----
 parsing/pcoq.ml      | 7 -------
 4 files changed, 24 deletions(-)

(limited to 'parsing')

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index f25b394f0b..18942ac295 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -114,9 +114,6 @@ module Error = struct
          | UnsupportedUnicode x ->
              Printf.sprintf "Unsupported Unicode character (0x%x)" x)
 
-  (* Require to fix the Camlp4 signature *)
-  let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
-
 end
 open Error
 
@@ -153,10 +150,6 @@ let bump_loc_line_last loc bol_pos =
   in
   Ploc.encl loc loc'
 
-let set_loc_file loc fname =
-  Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc)
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
 (* For some reason, the [Ploc.after] function of Camlp5 does not update line
    numbers, so we define our own function that does it. *)
 let after loc =
@@ -434,7 +427,6 @@ let push_char c =
     real_push_char c
 
 let push_string s = Buffer.add_string current_comment s
-let push_bytes s = Buffer.add_bytes current_comment s
 
 let null_comment s =
   let rec null i =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 496b200020..65e99d1b90 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -80,10 +80,6 @@ let create_pos = function
   | None -> Extend.First
   | Some lev -> Extend.After (constr_level lev)
 
-type gram_level =
-  gram_position option * gram_assoc option * string option *
-  (** for reinitialization: *) gram_reinit option
-
 let find_position_gen current ensure assoc lev =
   match lev with
   | None ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 011565d86a..3438635cfa 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -756,11 +756,6 @@ GEXTEND Gram
                  implicit_status = MaximallyImplicit}) items
     ]
   ];
-  name_or_bang: [
-       [ b = OPT "!"; id = name ->
-       not (Option.is_empty b), id
-    ]
-  ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
     [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index dad98e2e98..3f014c4c84 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -171,7 +171,6 @@ module Symbols : sig
   val sopt : G.symbol -> G.symbol
   val snterml : G.internal_entry * string -> G.symbol
   val snterm : G.internal_entry -> G.symbol
-  val snterml_level : G.symbol -> string
 end = struct
 
   let stoken tok =
@@ -199,10 +198,6 @@ end = struct
   let slist1 x = Gramext.Slist1 x
   let sopt x = Gramext.Sopt x
 
-  let snterml_level = function
-  | Gramext.Snterml (_, l) -> l
-  | _ -> failwith "snterml_level"
-
 end
 
 let camlp4_verbosity silent f x =
@@ -211,8 +206,6 @@ let camlp4_verbosity silent f x =
   f x;
   warning_verbose := a
 
-let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x
-
 (** Grammar extensions *)
 
 (** NB: [extend_statment =
-- 
cgit v1.2.3


From 9be835c4f16b3bc08ff9540a6854ced2d8185cb2 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:09:05 +0200
Subject: Remove unused constructors

---
 parsing/cLexer.ml4 | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 18942ac295..4629058083 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -99,7 +99,6 @@ module Error = struct
     | Unterminated_string
     | Undefined_token
     | Bad_token of string
-    | UnsupportedUnicode of int
 
   exception E of t
 
@@ -110,9 +109,7 @@ module Error = struct
          | Unterminated_comment -> "Unterminated comment"
          | Unterminated_string -> "Unterminated string"
          | Undefined_token -> "Undefined token"
-         | Bad_token tok -> Format.sprintf "Bad token %S" tok
-         | UnsupportedUnicode x ->
-             Printf.sprintf "Unsupported Unicode character (0x%x)" x)
+         | Bad_token tok -> Format.sprintf "Bad token %S" tok)
 
 end
 open Error
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 parsing/egramcoq.ml  | 1 -
 parsing/egramcoq.mli | 8 --------
 parsing/g_prim.ml4   | 1 -
 parsing/g_proofs.ml4 | 1 -
 4 files changed, 11 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 65e99d1b90..86c66ec5f1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Pcoq
 open Constrexpr
-open Notation
 open Notation_term
 open Extend
 open Libnames
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 6dda3817ae..0a0430ba6c 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -6,14 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constrexpr
-open Notation_term
-open Pcoq
-open Extend
-open Genarg
-open Egramml
-
 (** Mapping of grammar productions to camlp4 actions *)
 
 (** This is the part specific to Coq-level Notation and Tactic Notation.
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2af4ed533b..abb463f821 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,6 @@
 
 open Names
 open Libnames
-open Tok (* necessary for camlp4 *)
 
 open Pcoq
 open Pcoq.Prim
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7ca2e4a4f7..68b8be6b87 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -9,7 +9,6 @@
 open Constrexpr
 open Vernacexpr
 open Misctypes
-open Tok
 
 open Pcoq
 open Pcoq.Prim
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 parsing/pcoq.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 3f014c4c84..9a4766c0bf 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open CErrors
 open Util
 open Extend
-- 
cgit v1.2.3


From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 parsing/g_constr.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f2ed88fea..15f100c3b0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -146,12 +146,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
+      | "Type"; "@{"; u = universe; "}" -> GType u
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
-      | id = identref -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
+      | id = name -> [id]
       ] ]
   ;
   lconstr:
@@ -298,7 +298,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
+      | id = name -> GType (Some id)
       ] ]
   ;
   fix_constr:
-- 
cgit v1.2.3


From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:30:09 +0200
Subject: Adding support for using grammar entries returning no value in
 EXTEND.

---
 parsing/egramml.ml  | 4 ++--
 parsing/egramml.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 97a3e89a59..984957589f 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+      Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 | GramNonTerminal (_, t, tok) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let inj = Some (fun obj -> Genarg.in_gen t obj) in
+  let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1ad9472007..29baaf052b 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,7 +15,7 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option *
       ('s, 'a) Extend.symbol -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-- 
cgit v1.2.3


From 3c0d8d08bda81b9fbd7210e4e352a08bbe8219e8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 20:55:32 +0200
Subject: [vernac] Remove `Save.` command.

It has been deprecated for a while in favor of `Qed`.
---
 parsing/g_proofs.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 68b8be6b87..53637439a8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -48,7 +48,6 @@ GEXTEND Gram
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
-      | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
 	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 parsing/g_proofs.ml4 | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 53637439a8..2def222905 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -48,13 +48,11 @@ GEXTEND Gram
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
-      | IDENT "Save"; tok = thm_token; id = identref ->
-	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-	  VernacEndProof (Proved (Opaque None,Some (id,None)))
+	  VernacEndProof (Proved (Opaque None, Some id))
       | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
       |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (Transparent,Some (id,None)))
+	  VernacEndProof (Proved (Transparent,Some id))
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
-- 
cgit v1.2.3