From f68638477459eef68fb69adee244f58894e1f0a4 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Tue, 29 Jun 2004 15:55:40 +0000
Subject: moved instantiate binding to extratactics

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/pptacticnew.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'translate')

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 23092a733e..8855dda460 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -539,7 +539,7 @@ and pr_atom1 env = function
              hov 1 (str"(" ++ pr_id id ++ str " :=" ++
                     pr_lconstrarg env c ++ str")") ++
              pr_clauses pr_ident cl)
-  | TacInstantiate (n,c,ConclLocation ()) ->
+(*  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
                     pr_lconstrarg env c ++ str ")" ))
@@ -548,7 +548,7 @@ and pr_atom1 env = function
              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
                     pr_lconstrarg env c ++ str ")" ) 
 	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
-
+*)
   (* Derived basic tactics *)
   | TacSimpleInduction (h,l) ->
       if List.exists (fun (pp,_) -> !pp) !l then
-- 
cgit v1.2.3