From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

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

(limited to 'tactics/auto.mli')

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 50460de17a..b65d2ea218 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -85,8 +85,7 @@ val make_resolves :
    Never raises an User_exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
-val make_resolve_hyp : identifier -> constr
-      -> (constr_label * pri_auto_tactic) list
+val make_resolve_hyp : var_declaration -> (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
@@ -97,7 +96,7 @@ val make_extern :
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
 
-val make_local_hint_db : constr signature -> Hint_db.t
+val make_local_hint_db : var_context -> Hint_db.t
 
 val priority : (int * 'a) list -> 'a list
 
-- 
cgit v1.2.3