diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 10:07:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 10:07:47 +0100 |
| commit | 1cf756712b5a5216e3a0039fb9d831c8d8ba9cbf (patch) | |
| tree | 1cadeb96cce15c51dd6ffd217e3242657a11d70f /vernac | |
| parent | 8e9d1421354d55bc2ea71e37715a19d33cc9bc9c (diff) | |
| parent | b60906cc3ee3f994babf9cceff2971bd03485f2f (diff) | |
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use camlp4
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 4 | ||||
| -rw-r--r-- | vernac/metasyntax.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1bb9e0da1..3be357598 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -606,8 +606,8 @@ let distribute a ll = List.map (fun l -> a @ l) ll t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) let expand_list_rule typ tkl x n p ll = - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index b3049f1b7..e064b570e 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -51,7 +51,7 @@ val add_syntax_extension : val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit -(** Print the Camlp4 state of a grammar *) +(** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t |