diff options
| author | coq | 2002-10-01 07:53:07 +0000 |
|---|---|---|
| committer | coq | 2002-10-01 07:53:07 +0000 |
| commit | 02f6cb08e4b8f892594934766a40413a3fa30342 (patch) | |
| tree | 6c8e85d78ffbad43aa579ec3612cb93b14f1b4b2 /pretyping/pattern.mli | |
| parent | e6afa737d4bcc1c7973cd46094e824b875fede11 (diff) | |
Vraie substitutivite de autohints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 5ff667f90b..943a8d8c3d 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -35,6 +35,8 @@ type constr_pattern = val occur_meta_pattern : constr_pattern -> bool +val subst_pattern : substitution -> constr_pattern -> constr_pattern + type constr_label = | ConstNode of constant | IndNode of inductive @@ -43,6 +45,8 @@ type constr_label = val label_of_ref : global_reference -> constr_label +val subst_label : substitution -> constr_label -> constr_label + exception BoundPattern (* [head_pattern_bound t] extracts the head variable/constant of the |