From e867509591c1e8fad3fd764da652deb28d293d49 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 30 Apr 2000 00:53:51 +0000 Subject: Suite intégration de constr_pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacticals.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/tacticals.mli') diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index ac118b6d1..24b705ac7 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -52,8 +52,8 @@ val clause_type : clause -> goal sigma -> constr val matches : goal sigma -> constr -> marked_term -> bool val dest_match : goal sigma -> constr -> marked_term -> constr list *) -val gl_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list -val gl_is_matching : goal sigma -> constr_pattern -> constr -> bool +val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list +val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val allHyps : goal sigma -> clause list val afterHyp : identifier -> goal sigma -> clause list -- cgit v1.2.3