From 602b6e5f3e57f6a818e672dc967bde86a684ace2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Oct 2003 19:10:39 +0000
Subject: Typo

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5a8ce22424..98e36520a8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -319,7 +319,7 @@ let rec intros_using = function
 
 let intros = tclREPEAT (intro_force false)
 
-let intro_erasing id = tclTHEN (thin [id]) (intro_using id gl)
+let intro_erasing id = tclTHEN (thin [id]) (intro_using id)
 
 let intros_replacing ids gls = 
   let rec introrec = function
-- 
cgit v1.2.3