diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9f7491d5f4..9db1c7dc42 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1609,8 +1609,8 @@ let rec xlate_vernac = | VernacDeclareTacticDefinition (true, tacs) -> (match List.map (function - ((_, id), _, body) -> - CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) + (id, _, body) -> + CT_tac_def(reference_to_ct_ID id, xlate_tactic body)) tacs with [] -> assert false | fst::tacs1 -> |