From 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Sep 2014 09:13:40 +0200
Subject: Add syntax for naming new goals in refine: writing ?[id] instead of _
 will name the goal id; writing ?[?id] will use the first fresh name available
 based with prefix id.

Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/ppvernac.ml')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b841c19cc3..a5235a25fa 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -236,7 +236,7 @@ let pr_module_binders l pr_c =
   prlist_strict (pr_module_vardecls pr_c) l
 
 let pr_type_option pr_c = function
-  | CHole (loc, k, _) -> mt()
+  | CHole (loc, k, Misctypes.IntroAnonymous, _) -> mt()
   | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
 let pr_decl_notation prc ((loc,ntn),c,scopt) =
-- 
cgit v1.2.3