aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-30 09:13:40 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-30 09:30:53 +0200
commit538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f (patch)
tree53478ded9dfb8108402d7f45fa1300edd1569a20 /interp/notation.ml
parent2bbf1305a080667d8547c44b2684010aba3d8d45 (diff)
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.
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 93e6f31c0..de7eca352 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,[])