From dfa78c4fdd1ec8755010b64ec5494f4efa71bd4d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 Sep 2003 18:43:05 +0000
Subject: Traduction de Instantiate

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

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a03a8c2466..9c7b627c87 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -272,7 +272,7 @@ and pr_atom1 env = function
       hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str " :=" ++
         pr_constrarg env c ++ pr_clause_pattern pr_ident cl)
   | TacInstantiate (n,c) ->
-      hov 1 (str "instantiate" ++ pr_arg int n ++ pr_lconstrarg env c)
+      hov 1 (str "instantiate" ++ pr_arg int n ++ pr_constrarg env c)
 
   (* Derived basic tactics *)
   | TacOldInduction h ->
-- 
cgit v1.2.3