diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-07 17:41:10 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-07 17:41:10 +0000 |
| commit | 22cb4d34d7f67eb98c737b076a4ecbbf800bdc55 (patch) | |
| tree | 9a238c0c4919245db39f805056754b1798e94357 /pretyping/pattern.mli | |
| parent | e2363aafc80d9a8efaf9c13bbf9e4e5bb0f4eb10 (diff) | |
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 398117303..7ce0c4124 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -52,28 +52,18 @@ val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern -type constr_label = - | ConstNode of constant - | IndNode of inductive - | CstrNode of constructor - | VarNode of identifier - -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 type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly if [t] is an abstraction *) -val head_pattern_bound : constr_pattern -> constr_label +val head_pattern_bound : constr_pattern -> global_reference (* [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) -val head_of_constr_reference : Term.constr -> constr_label +val head_of_constr_reference : Term.constr -> global_reference (* [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no |