From 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 13 Oct 2014 14:35:07 +0200
Subject: Goal: remove most of the API (make [Goal.goal] concrete).

We are left with the compatibility layer and a handful of primitives which require some thought to move.
---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0e082077fe..cba33929b9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -397,7 +397,7 @@ let display_name = false
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-  if display_name then str " " ++ Pp.surround (pr_id (Goal.goal_ident sigma g))
+  if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
   else mt ()
 
 (* display the conclusion of a goal *)
-- 
cgit v1.2.3