From 4dc7a3eb4ac669ead5ee4a1986c4a2310ffda911 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Jan 2003 22:06:34 +0000
Subject: Restructuration interpréteur de tactique: plus d'évaluation partielle
 à la définition; suppression TacFunRec, VClosure, VFTactic et VContext;
 davantage de globalisation statique (notamment pour les tactiques
 mutuellement récursives); débogueur plus informatif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/eauto.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5667796fee..bb965213b8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -349,10 +349,10 @@ open Genarg
 let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases"
 let hintbases = create_generic_entry "hintbases" rawwit_hintbases
 let _ = Tacinterp.add_genarg_interp "hintbases"
-  (fun ist x ->
+  (fun ist gl x ->
     (in_gen wit_hintbases
       (out_gen (wit_opt (wit_list0 wit_string))
-	(Tacinterp.genarg_interp ist
+	(Tacinterp.genarg_interp ist gl
 	  (in_gen (wit_opt (wit_list0 rawwit_string))
 	    (out_gen rawwit_hintbases x))))))
 
-- 
cgit v1.2.3