diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index ecb04e0755..e8fd52dba8 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -978,7 +978,7 @@ and xlate_tac = let id_opt = match out_gen Extratactics.rawwit_in_arg_hyp id_opt with | None -> ctv_ID_OPT_NONE - | Some id -> ctf_ID_OPT_SOME (xlate_ident id) + | Some (_,id) -> ctf_ID_OPT_SOME (xlate_ident id) in let tac_opt = match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with |