diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 8 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f1b8eee5e2..881482081a 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -397,11 +397,11 @@ let create_ltac_quotation name cast (e, l) = let assoc = None in let rule = Next (Next (Next (Next (Next (Stop, - Atoken (Lexer.terminal name)), - Atoken (Lexer.terminal ":")), - Atoken (Lexer.terminal "(")), + Atoken (CLexer.terminal name)), + Atoken (CLexer.terminal ":")), + Atoken (CLexer.terminal "(")), entry), - Atoken (Lexer.terminal ")")) + Atoken (CLexer.terminal ")")) in let action _ v _ _ _ loc = cast (loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6a5d1380d6..d650cb5c6f 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -552,7 +552,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 |