From 667e4a7870625bc8dedb651b278cbca4f43e793d Mon Sep 17 00:00:00 2001
From: gregoire
Date: Thu, 12 Dec 2002 15:42:49 +0000
Subject: Ajout du vernac Proof with

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

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a09bfbd120..efc2a9b822 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1695,7 +1695,10 @@ let interp_tacarg sign ast = (*unvarg*) (val_interp sign ast)
 let interp = fun ast -> tac_interp [] [] !debug ast
 
 (* Hides interpretation for pretty-print *)
-let hide_interp t = abstract_tactic_expr (TacArg (Tacexp t)) (interp t)
+let hide_interp t ot =  
+  match ot with 
+  | None -> abstract_tactic_expr (TacArg (Tacexp t)) (interp t)
+  | Some t' -> abstract_tactic_expr (TacArg (Tacexp t)) (tclTHEN (interp t) t')
 
 (* For bad tactic calls *)
 let bad_tactic_args s =
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index b4b666fa75..c22ce9829c 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -103,7 +103,8 @@ val constr_interp : interp_sign -> constr_expr -> constr
 val interp : raw_tactic_expr -> tactic
 
 (* Hides interpretation for pretty-print *)
-val hide_interp : raw_tactic_expr -> tactic
+
+val hide_interp : raw_tactic_expr -> tactic option -> tactic
 
 (* Adds an interpretation function *)
 val interp_add : string * (interp_sign -> Coqast.t -> value) -> unit
-- 
cgit v1.2.3