diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-21 12:50:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-21 14:31:33 +0200 |
| commit | 426ba79b270299f64a4498187adad717760d11bc (patch) | |
| tree | 4344bc96a41f16cc139e1751362dda8ae90a47e4 | |
| parent | de2031b8fa2a7e236d734500294ebd5050fcb7d5 (diff) | |
Expliciting some uses of Compat module.
| -rw-r--r-- | parsing/lexer.ml4 | 11 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 3 |
2 files changed, 6 insertions, 8 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index c6d5f3b92..23bd74da9 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -8,7 +8,6 @@ open Pp open Util -open Compat open Tok (* Dictionaries: trees annotated with string options, each node being a map @@ -565,7 +564,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc let current_location_table = ref (loct_create ()) -type location_table = (int, CompatLoc.t) Hashtbl.t +type location_table = (int, Compat.CompatLoc.t) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t @@ -602,7 +601,7 @@ let func cs = Stream.from (fun i -> let (tok, loc) = next_token cs in - loct_add loct i (make_loc loc); Some tok) + loct_add loct i (Compat.make_loc loc); Some tok) in current_location_table := loct; (ts, loct_func loct) @@ -622,10 +621,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *) module M_ = Camlp4.ErrorHandler.Register (Error) -module Loc = CompatLoc +module Loc = Compat.CompatLoc module Token = struct include Tok (* Cf. tok.ml *) - module Loc = CompatLoc + module Loc = Compat.CompatLoc module Error = Camlp4.Struct.EmptyError module Filter = struct type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t @@ -643,7 +642,7 @@ let mk () _init_loc(*FIXME*) cs = let rec self = parser i [< (tok, loc) = next_token; s >] -> - let loc = make_loc loc in + let loc = Compat.make_loc loc in loct_add loct i loc; [< '(tok, loc); self s >] | [< >] -> [< >] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2146ad964..6e9cf263f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -14,13 +14,12 @@ open Genarg open Constrexpr open Tacexpr open Libnames -open Compat open Misctypes open Genredexpr (** The parser of Coq *) -module Gram : GrammarSig +module Gram : Compat.GrammarSig (** The parser of Coq is built from three kinds of rule declarations: |