diff options
Diffstat (limited to 'plugins/ltac/profile_ltac.ml')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3ff7b53c7..020b3048f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Unicode open Pp open Printer @@ -113,7 +114,7 @@ let rec to_ltacprof_tactic m xml = children = List.fold_left to_ltacprof_tactic M.empty xs; } in M.add name node m - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.") let to_ltacprof_results xml = let open Xml_datatype in @@ -125,7 +126,7 @@ let to_ltacprof_results xml = max_total = 0.0; local = 0.0; children = List.fold_left to_ltacprof_tactic M.empty xs } - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.") let feedback_results results = Feedback.(feedback @@ -246,7 +247,7 @@ let string_of_call ck = (match ck with | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) (Tacexpr.TacAtom (Loc.tag te))) |