From a008023cae4fdddffbbbfd8a455d7776200a9cfb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 6 Nov 2003 14:35:25 +0000
Subject: Added Instantiate ... in

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

(limited to 'translate')

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 0dbc082504..035cdfd635 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -455,11 +455,15 @@ and pr_atom1 env = function
              hov 1 (str"(" ++ pr_id id ++ str " :=" ++
                     pr_lconstrarg env c ++ str")") ++
              pr_clause_pattern pr_ident cl)
-  | TacInstantiate (n,c) ->
+  | TacInstantiate (n,c,None) ->
       hov 1 (str "instantiate" ++ spc() ++
              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-                    pr_lconstrarg env c ++ str")"))
-
+                    pr_lconstrarg env c ++ str ")"))
+ | TacInstantiate (n,c,Some id) ->
+      hov 1 (str "instantiate" ++ spc() ++
+             hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+                    pr_lconstrarg env c ++ str ")" ++ 
+		    spc () ++ str "in" ++ pr_arg pr_ident id))
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h)
-- 
cgit v1.2.3