diff options
| author | Emilio Jesus Gallego Arias | 2018-02-14 02:06:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-01 01:44:12 +0100 |
| commit | ba27c2e21f80b41dfd837e6c6b15f82ca405cf04 (patch) | |
| tree | 679e347ebcefda7a020cebf0044825c72b88c9ee | |
| parent | 5cb74f82165e88c5e527ad757b007df1fbe5f1b3 (diff) | |
[coq] Adapt to coq/coq#6511
coq/coq#6511 contains EConstr-related changes.
| -rw-r--r-- | src/tac2entries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index e48bf02321..fa498ab44f 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -344,7 +344,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = in let () = if exists then - user_err ?loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists") + user_err ?loc (str "Tactic " ++ Names.Id.print id ++ str " already exists") in (id, e, t) in @@ -539,7 +539,7 @@ let parse_scope = function if Id.Map.mem id !scope_table then Id.Map.find id !scope_table toks else - CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id) + CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id) | SexprStr (_, str) -> let v_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0)) in ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit)) |