aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/pre_parser_aux.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-03-09 11:38:07 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2018-03-09 11:38:07 +0100
commit3f12f94bb84b796f764a2a0765048c17ab840ffb (patch)
tree15afe176f482b672c71587ec49a73605619962fc /cparser/pre_parser_aux.ml
parent31caa091ba19b8216dc7d26cfc47530c860514fa (diff)
downloadcompcert-kvx-3f12f94bb84b796f764a2a0765048c17ab840ffb.tar.gz
compcert-kvx-3f12f94bb84b796f764a2a0765048c17ab840ffb.zip
Add explicit interface to cparser/pre_parser_aux.ml
This should help with parallel builds, which currently fail sometimes owing to a lack of a dependency on pre_parser_aux.cmi. Also: move documentation comments from the .ml to the .mli
Diffstat (limited to 'cparser/pre_parser_aux.ml')
-rw-r--r--cparser/pre_parser_aux.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/cparser/pre_parser_aux.ml b/cparser/pre_parser_aux.ml
index 74bf494c..4a4953ba 100644
--- a/cparser/pre_parser_aux.ml
+++ b/cparser/pre_parser_aux.ml
@@ -18,11 +18,6 @@ type identifier_type =
| TypedefId
| OtherId
-(* Applying once this functions saves the current context, and
- applying it the second time restores it. *)
let save_context:(unit -> (unit -> unit)) ref = ref (fun _ -> assert false)
-
-(* Change the context by changing an identifier to be a varname or a
- typename *)
let declare_varname:(string -> unit) ref = ref (fun _ -> assert false)
let declare_typename:(string -> unit) ref = ref (fun _ -> assert false)