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

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 93e6f31c03..de7eca352f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -442,7 +442,7 @@ let interp_prim_token =
 
 let rec rcp_of_glob looked_for = function
   | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_,_) -> RCPatAtom (loc,None)
+  | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
   | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
   | GApp (loc,GRef (_,g,_),l) ->
     looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
-- 
cgit v1.2.3