diff options
| author | Pierre-Marie Pédrot | 2016-05-09 16:33:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-09 16:35:49 +0200 |
| commit | a66b57ba4bba866bb626bde2b6fe3b762347eb3e (patch) | |
| tree | 7e78979db8010c5221352cb7fcbcc12a8be3db62 /tactics | |
| parent | b43956fe19177a178dfbcef0b173ebada5060973 (diff) | |
Rename Lexer -> CLexer.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5ecc46d670..a7acdf7594 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -491,7 +491,7 @@ let interp_fresh_id ist env sigma l = String.concat "" (List.map (function | ArgArg s -> s | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in - let s = if Lexer.is_keyword s then s^"0" else s in + let s = if CLexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env |