From 33a06cfbb9f035000379f7d994aa6ab10e7ffb66 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 28 Jun 2004 14:27:59 +0000
Subject: more evar stuff

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

(limited to 'translate')

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 90c0145e8a..23092a733e 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -539,11 +539,16 @@ 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,cls) ->
+  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-                    pr_lconstrarg env c ++ str ")" ++ 
-		    pr_clauses pr_ident cls))
+                    pr_lconstrarg env c ++ str ")" ))
+  | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             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