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.

3 files changed, 19 insertions, 11 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ce7f5959a..631c2428e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -22,7 +22,7 @@ type goal = {
 			      logical information once put together
 			      with an evar_map. *)
   tags : string list;
-  (** Heriditary? tags to be displayed *)
+  (** Hereditary? tags to be displayed *)
   cache : Evd.evar_map;
   (** Invariant: for all sigma, if gl.cache == sigma and gl.content is actually
       pertaining to sigma, then gl is nf-evarized in sigma. We use this not to
@@ -246,6 +246,11 @@ module V82 = struct
   let partial_solution sigma { content=evk } c =
     Evd.define evk c sigma
 
+  (* Instantiates a goal with an open term, using name of goal for evk' *)
+  let partial_solution_to sigma { content=evk } { content=evk' } c =
+    let id = Evd.evar_ident evk sigma in
+    Evd.rename evk' id (Evd.define evk c sigma)
+
   (* Parts of the progress tactical *)
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = content evars1 gl1 in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 4d4d0c2eb..d31a51fbd 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -94,10 +94,13 @@ module V82 : sig
       stuff. *)
   val build : Evd.evar -> goal 
 
-
   (* Instantiates a goal with an open term *)
   val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
-   
+
+  (* Instantiates a goal with an open term, reusing name of goal for
+     second goal *)
+  val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+
   (* Principal part of the weak-progress tactical *)
   val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
    
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b9cff0527..008df0096 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -530,14 +530,14 @@ let prim_refiner r sigma goal =
 	       let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
                let sigma = 
-		 Goal.V82.partial_solution sigma goal (mkNamedLambda id c1 ev) in
+		 Goal.V82.partial_solution_to sigma goal sg (mkNamedLambda id c1 ev) in
 	       ([sg], sigma)
 	   | LetIn (_,c1,t1,b) ->
 	       let (sg,ev,sigma) =
 		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       let sigma = 
-		 Goal.V82.partial_solution sigma goal (mkNamedLetIn id c1 t1 ev) in
+		 Goal.V82.partial_solution_to sigma goal sg (mkNamedLetIn id c1 t1 ev) in
 	       ([sg], sigma)
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
@@ -559,7 +559,7 @@ let prim_refiner r sigma goal =
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
 	let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
+	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | FixRule (f,n,rest,j) ->
@@ -661,12 +661,12 @@ let prim_refiner r sigma goal =
         let (sg,ev,sigma) = mk_goal sign cl' in
 	let sigma = check_conv_leq_goal env sigma cl' cl' cl in
 	let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
+	let sigma = Goal.V82.partial_solution_to sigma goal sg ev in
           ([sg], sigma)
 
     | Convert_hyp (id,copt,ty) ->
 	let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
+	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
 	([gl], sigma)
 
     (* And now the structural rules *)
@@ -676,7 +676,7 @@ let prim_refiner r sigma goal =
 	let (gl,ev,sigma) =
 	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
 	in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
+	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
 	  ([gl], sigma)
 
     | Move (withdep, hfrom, hto) ->
@@ -685,7 +685,7 @@ let prim_refiner r sigma goal =
   	let hyps' =
 	  move_hyp withdep toleft (left,declfrom,right) hto in
 	let (gl,ev,sigma) = mk_goal hyps' cl in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
+	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
   	  ([gl], sigma)
 
     | Rename (id1,id2) ->
@@ -698,5 +698,5 @@ let prim_refiner r sigma goal =
         let cl' = replace_vars [id1,mkVar id2] cl in
 	let (gl,ev,sigma) = mk_goal sign' cl' in
 	let ev = Vars.replace_vars [(id2,mkVar id1)] ev in
-	let sigma = Goal.V82.partial_solution sigma goal ev in
+	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
           ([gl], sigma)