From b60906cc3ee3f994babf9cceff2971bd03485f2f Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 22 Jan 2018 12:45:49 -0800 Subject: Change references to CAMLP4 to CAMLP5 to be more accurate since we no longer use camlp4. --- parsing/pcoq.ml | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'parsing/pcoq.ml') 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] -- cgit v1.2.3