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.
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 95cfd73a04..a23b1b64af 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -53,7 +53,7 @@ let rec under_binders env f n c =
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
   | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
-  | CHole (loc, k, _) ->
+  | CHole (loc, k, _, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
 	user_err_loc (loc,"",
-- 
cgit v1.2.3