aboutsummaryrefslogtreecommitdiff
path: root/printing/proof_diffs.ml
diff options
context:
space:
mode:
authorHugo Herbelin2018-12-05 19:41:48 +0100
committerHugo Herbelin2019-01-06 19:45:57 +0100
commit9d6188637570d6fa62c74aecc95212821bcb22df (patch)
treee78f9acdfd75d174cf0ff4a27f25404b46608815 /printing/proof_diffs.ml
parent3d7eb01d428c9d98b10004f3f4f40b2209232971 (diff)
Renaming pr_evar_suggested_name into -> evar_suggested_name.
Since it returns an Id.t and not a Pp.t.
Diffstat (limited to 'printing/proof_diffs.ml')
-rw-r--r--printing/proof_diffs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index c1ea067567..878e9f477b 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -546,7 +546,7 @@ let to_constr p =
module GoalMap = Evar.Map
-let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
+let goal_to_evar g sigma = Id.to_string (Termops.evar_suggested_name g sigma)
open Goal.Set