diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /pretyping/patternops.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'pretyping/patternops.mli')
-rw-r--r-- | pretyping/patternops.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 9f087857..36317b3a 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -8,12 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open EConstr -open Globnames -open Glob_term +open Names open Mod_subst -open Misctypes +open Glob_term open Pattern +open EConstr open Ltac_pretype (** {5 Functions on patterns} *) @@ -32,12 +31,12 @@ exception BoundPattern 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 +val head_pattern_bound : constr_pattern -> GlobRef.t (** [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) -val head_of_constr_reference : Evd.evar_map -> constr -> global_reference +val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t (** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no |