diff options
| author | Pierre-Marie Pédrot | 2016-05-09 18:37:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-09 18:40:35 +0200 |
| commit | cd9f2859e69d99aea5b29a6d677448a39a234b6f (patch) | |
| tree | 500a8b0d1c36662f590c7956cf932663028186be /ltac | |
| parent | 4114926d5bf60b014c363788d043c00184655da2 (diff) | |
| parent | aa6a7fc837f8148655c179e9a0b63c3044edfe71 (diff) | |
Merge branch 'v8.5'
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 |