diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 28 |
1 files changed, 13 insertions, 15 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index e7460377b..33105c312 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Pp open Names open Sign @@ -18,14 +17,13 @@ open Libnames open Nametab open Rawterm open Mod_subst -(*i*) -(* Pattern variables *) +(** Pattern variables *) type patvar_map = (patvar * constr) list val pr_patvar : patvar -> std_ppcmds -(* Patterns *) +(** Patterns *) type constr_pattern = | PRef of global_reference @@ -51,24 +49,24 @@ val subst_pattern : substitution -> constr_pattern -> constr_pattern exception BoundPattern -(* [head_pattern_bound t] extracts the head variable/constant of the +(** [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 -> global_reference -(* [head_of_constr_reference c] assumes [r] denotes a reference and +(** [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 -> global_reference -(* [pattern_of_constr c] translates a term [c] with metavariables into +(** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern -(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into +(** [pattern_of_rawconstr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they are bound *) |