Change references to CAMLP4 to CAMLP5 to be more accurate since we no

longer use camlp4.

8 files changed, 37 insertions, 37 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9c2766187..ea6266dd4 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -21,11 +21,11 @@ open Names
    a reference to the current level (to be translated into "SELF" on the
    left border and into "constr LEVEL n" elsewhere), to the level below
    (to be translated into "NEXT") or to an below wrt associativity (to be
-   translated in camlp4 into "constr" without level) or to another level
+   translated in camlp5 into "constr" without level) or to another level
    (to be translated into "constr LEVEL n")
 
    The boolean is true if the entry was existing _and_ empty; this to
-   circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
+   circumvent a weakness of camlp5 whose undo mechanism is not the
    converse of the extension mechanism *)
 
 let constr_level = string_of_int
@@ -144,11 +144,11 @@ let find_position accu forpat assoc level =
 
 (**************************************************************************)
 (*
- * --- Note on the mapping of grammar productions to camlp4 actions ---
+ * --- Note on the mapping of grammar productions to camlp5 actions ---
  *
  * Translation of environments: a production
  *   [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
- * is written (with camlp4 conventions):
+ * is written (with camlp5 conventions):
  *   (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
  * where v1..vi are the values generated by non-terminals nt1..nti.
  * Since the actions are executed by substituting an environment,
@@ -172,8 +172,8 @@ let find_position accu forpat assoc level =
 (**********************************************************************)
 (* Binding constr entry keys to entries                               *)
 
-(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp4_assoc = function
+(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *)
+let camlp5_assoc = function
   | Some NonA | Some RightA -> RightA
   | None | Some LeftA -> LeftA
 
@@ -205,7 +205,7 @@ let adjust_level assoc from = function
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
   | (NumLevel n,BorderProd (Left,Some NonA)) -> None
   (* If the expected assoc is the current one, set to SELF *)
-  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
+  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
       None
   (* Otherwise, force the level, n or n-1, according to expected assoc *)
   | (NumLevel n,BorderProd (Left,Some a)) ->
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 8e0469275..1e3869818 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Mapping of grammar productions to camlp4 actions *)
+(** Mapping of grammar productions to camlp5 actions *)
 
 (** This is the part specific to Coq-level Notation and Tactic Notation.
     For the ML-level tactic and vernac extensions, see Egramml. *)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 7414773d3..74dd95a20 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -8,7 +8,7 @@
 
 open Vernacexpr
 
-(** Mapping of grammar productions to camlp4 actions. *)
+(** Mapping of grammar productions to camlp5 actions. *)
 
 (** This is the part specific to vernac extensions.
     For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3244b0ff2..d42b5f622 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -17,7 +17,7 @@ open Vernacexpr
 open Decl_kinds
 open Declarations
 open Misctypes
-open Tok (* necessary for camlp4 *)
+open Tok (* necessary for camlp5 *)
 
 open Pcoq
 open Pcoq.Prim
@@ -827,7 +827,7 @@ GEXTEND Gram
   command:
     [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
-      (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
+      (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
 	 info = hint_info ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index c934d38a2..54e7949ae 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -202,7 +202,7 @@ end = struct
 
 end
 
-let camlp4_verbosity silent f x =
+let camlp5_verbosity silent f x =
   let a = !warning_verbose in
   warning_verbose := silent;
   f x;
@@ -274,7 +274,7 @@ type ext_kind =
 
 (** The list of extensions *)
 
-let camlp4_state = ref []
+let camlp5_state = ref []
 
 (** Deletion *)
 
@@ -299,13 +299,13 @@ let grammar_delete e reinit (pos,rls) =
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e reinit ext in
-  let redo () = camlp4_verbosity false (uncurry (G.extend e)) ext in
-  camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
+  let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in
+  camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e reinit ext =
-  camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
-  camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
+  camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
+  camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -315,20 +315,20 @@ module Gram =
     include G
     let extend e =
       curry
-	(fun ext ->
-	   camlp4_state :=
-	     (ByEXTEND ((fun () -> grammar_delete e None ext),
-			(fun () -> uncurry (G.extend e) ext)))
-	   :: !camlp4_state;
-	   uncurry (G.extend e) ext)
+    (fun ext ->
+      camlp5_state :=
+        (ByEXTEND ((fun () -> grammar_delete e None ext),
+           (fun () -> uncurry (G.extend e) ext)))
+      :: !camlp5_state;
+      uncurry (G.extend e) ext)
     let delete_rule e pil =
       (* spiwack: if you use load an ML module which contains GDELETE_RULE
-	  in a section, God kills a kitty. As it would corrupt remove_grammars.
+      in a section, God kills a kitty. As it would corrupt remove_grammars.
           There does not seem to be a good way to undo a delete rule. As deleting
-	  takes fewer arguments than extending. The production rule isn't returned
-	  by delete_rule. If we could retrieve the necessary information, then
-	  ByEXTEND provides just the framework we need to allow this in section.
-	  I'm not entirely sure it makes sense, but at least it would be more correct.
+      takes fewer arguments than extending. The production rule isn't returned
+      by delete_rule. If we could retrieve the necessary information, then
+      ByEXTEND provides just the framework we need to allow this in section.
+      I'm not entirely sure it makes sense, but at least it would be more correct.
           *)
       G.delete_rule e pil
   end
@@ -340,18 +340,18 @@ module Gram =
 
 let rec remove_grammars n =
   if n>0 then
-    (match !camlp4_state with
+    (match !camlp5_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
        | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
            grammar_delete g reinit (of_coq_extend_statement ext);
-           camlp4_state := t;
+           camlp5_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
            undo();
-           camlp4_state := t;
+           camlp5_state := t;
            remove_grammars n;
            redo();
-           camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+           camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state)
 
 let make_rule r = [None, None, r]
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 756d9487d..75378d2c6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -124,7 +124,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
         |
         | Egrammar.make_constr_prod_item
         V
-      Gramext.g_symbol list which is sent to camlp4
+      Gramext.g_symbol list which is sent to camlp5
 
     For user level tactic notations, dynamic addition of new rules is
     also done in several steps:
@@ -161,9 +161,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
 *)
 
-(** Temporarily activate camlp4 verbosity *)
+(** Temporarily activate camlp5 verbosity *)
 
-val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
+val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
 (** Parse a string *)
 
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 0917e8d6d..fafad2779 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -60,7 +60,7 @@ let match_keyword kwd = function
   | KEYWORD kwd' when kwd = kwd' -> true
   | _ -> false
 
-(* Needed to fix Camlp4 signature.
+(* Needed to fix Camlp5 signature.
  Cannot use Pp because of silly Tox -> Compat -> Pp dependency *)
 let print ppf tok = Format.pp_print_string ppf (to_string tok)
 
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 59a79dcd2..162310e2a 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -22,7 +22,7 @@ type t =
 val equal : t -> t -> bool
 val extract_string : t -> string
 val to_string : t -> string
-(* Needed to fit Camlp4 signature *)
+(* Needed to fit Camlp5 signature *)
 val print : Format.formatter -> t -> unit
 val match_keyword : string -> t -> bool
 (** for camlp5 *)