From d4f8643a9f5aff3c0f819b4b7aafda4b782ef55d Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 27 Oct 2000 16:28:55 +0000
Subject: erreur dans intro_gen corrigée

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3efb6393b5..e6b43a81e8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -285,7 +285,8 @@ let rec intro_gen name_flag move_flag force_flag gl =
         | IBasedOn (id,idl) -> fresh_id idl id gl
         | IMustBe id        -> 
 	    let id' = fresh_id [] id gl in
-  	    if id' <> id then error ((string_of_id id)^" is already used")
+  	    if id' <> id then error ((string_of_id id)^" is already used");
+	    id'
     in
     begin match move_flag with
       | None      -> introduction id gl
-- 
cgit v1.2.3