diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-30 00:53:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-30 00:53:51 +0000 |
| commit | e867509591c1e8fad3fd764da652deb28d293d49 (patch) | |
| tree | 020f62a4157a5b13ac8de4fcd6229f34e1971064 /tactics/tacticals.mli | |
| parent | de22ca2b88c8350f1f9e1e2b261c42844aea4367 (diff) | |
Suite intégration de constr_pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |