-
-let disambiguate_tactic lexicon_status_ref context metasenv tactic =
- let disambiguate_term = disambiguate_term lexicon_status_ref in
- let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in
- let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in
- let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in
+;;
+
+let disambiguate_tactic
+ lexicon_status_ref context metasenv (text,prefix_len,tactic)
+=
+ let disambiguate_term =
+ disambiguate_term text prefix_len lexicon_status_ref in
+ let disambiguate_pattern =
+ disambiguate_pattern text prefix_len lexicon_status_ref in
+ let disambiguate_reduction_kind =
+ disambiguate_reduction_kind text prefix_len lexicon_status_ref in
+ let disambiguate_lazy_term =
+ disambiguate_lazy_term text prefix_len lexicon_status_ref in