diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index cf0d4528..25a57ed2 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pattern.mli,v 1.17.2.1 2004/07/16 19:30:45 herbelin Exp $ i*) +(*i $Id: pattern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) (*i*) open Pp @@ -17,6 +17,7 @@ open Environ open Libnames open Nametab open Rawterm +open Mod_subst (*i*) (* Pattern variables *) @@ -24,10 +25,6 @@ open Rawterm type patvar_map = (patvar * constr) list val pr_patvar : patvar -> std_ppcmds -(* Only for v7 parsing/printing *) -val patvar_of_int : int -> patvar -val patvar_of_int_v7 : int -> patvar - (* Patterns *) type constr_pattern = @@ -51,28 +48,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 |