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

(limited to 'stm')

diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 415ea951f2..bd6f0fe9e8 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -429,7 +429,7 @@ and pp_expr ?(attr=[]) e =
         (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
           ppcel)
   | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
-  | CHole (loc, _, _) -> xmlCst ~attr  "_" loc
+  | CHole (loc, _, _, _) -> xmlCst ~attr  "_" loc
   | CIf (loc, test, (_, ret), th, el) ->
       let return = match ret with
       | None -> []
-- 
cgit v1.2.3