From d4edd135e7cb8b6f86d9d5a0d320e0b29ee20148 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2015 17:57:24 +0200
Subject: Preserving goal name in revert/bring_hyps.

---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0d6a26a113..1437b24625 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2480,11 +2480,13 @@ let bring_hyps hyps =
   else
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
+      let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
       Proofview.Refine.refine begin fun sigma ->
-        let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+        let (sigma, ev) =
+          Evarutil.new_evar env sigma ~principal:true ~store newcl in
         (sigma, (mkApp (ev, args)))
       end
     end
-- 
cgit v1.2.3