From 824bed965dbafbf740dca754380b532922cfb90b Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:42:32 +0000
Subject: Plug back infoH.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17037 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 238edd6593..0fcbf97ff6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1133,9 +1133,9 @@ and eval_tactic ist = function
       end
   | TacProgress tac -> Proofview.tclPROGRESS (interp_tactic ist tac)
   | TacShowHyps tac ->
-      (* arnaud: todo:
-         tclSHOWHYPS (interp_tactic ist tac)*)
-      assert false
+         Proofview.V82.tactic begin
+           tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
+         end
   | TacAbstract (tac,ido) ->
       Proofview.V82.tactic begin fun gl -> Tactics.tclABSTRACT
         (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl
-- 
cgit v1.2.3