diff options
| author | Pierre-Marie Pédrot | 2016-05-13 17:18:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 15:32:16 +0200 |
| commit | 9a33b2edbd1b44b37a423458de2970a174795650 (patch) | |
| tree | 5a91b36225d00d951e228aaa18ab69c9c27fcb38 /mathcomp | |
| parent | b40d797a0c1b667857364ebed489a6e87e7d3f98 (diff) | |
Fix compilation after the renaming of Lexer into CLexer.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index e75d40b..0bccc0c 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -16,7 +16,7 @@ let () = Mltop.add_known_plugin (fun () -> (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = Lexer.freeze () ;; +let frozen_lexer = CLexer.freeze () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) @@ -136,7 +136,7 @@ let pf_fresh_global name gl = let ssr_loaded = Summary.ref ~name:"SSR:loaded" false let is_ssr_loaded () = !ssr_loaded || - (if Lexer.is_keyword "SsrSyntax_is_Imported" then ssr_loaded:=true; + (if CLexer.is_keyword "SsrSyntax_is_Imported" then ssr_loaded:=true; !ssr_loaded) (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -1220,7 +1220,7 @@ let pr_ssr_search_item _ _ _ = pr_search_item (* Workaround the notation API that can only print notations *) -let is_ident s = try Lexer.check_ident s; true with _ -> false +let is_ident s = try CLexer.check_ident s; true with _ -> false let is_ident_part s = is_ident ("H" ^ s) @@ -6218,6 +6218,6 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Lexer.unfreeze frozen_lexer ;; +let () = CLexer.unfreeze frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index 7bd7f37..03dcb2f 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 @@ -3,7 +3,7 @@ (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = Lexer.freeze () ;; +let frozen_lexer = CLexer.freeze () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) @@ -1357,6 +1357,6 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = Lexer.unfreeze frozen_lexer ;; +let () = CLexer.unfreeze frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) |