diff options
| author | Pierre-Marie Pédrot | 2017-09-03 23:52:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 00:40:56 +0200 |
| commit | 102cfe76bc42d3139c79eca59eb782fcf644317b (patch) | |
| tree | 6f371c06566e7638fdb72c43c36bfa95f90724e6 /theories/Pattern.v | |
| parent | 34912844e18ef84d88af87e1dca05ab0426871c9 (diff) | |
Implementing lazy matching over terms.
Diffstat (limited to 'theories/Pattern.v')
| -rw-r--r-- | theories/Pattern.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/theories/Pattern.v b/theories/Pattern.v index ab3135f189..a672ad0fe7 100644 --- a/theories/Pattern.v +++ b/theories/Pattern.v @@ -14,7 +14,7 @@ Ltac2 Type context. Ltac2 Type 'a constr_match := [ | ConstrMatchPattern (pattern, constr array -> 'a) -| ConstrMatchContext (pattern, constr -> constr array -> 'a) +| ConstrMatchContext (pattern, context -> constr array -> 'a) ]. Ltac2 @ external matches : t -> constr -> (ident * constr) list := @@ -30,6 +30,14 @@ Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) li value compared to [matches] is the context of the match, to be filled with the instantiate function. *) +Ltac2 @ external matches_vect : t -> constr -> constr array := + "ltac2" "pattern_matches_vect". +(** Internal version of [matches] that does not return the identifiers. *) + +Ltac2 @ external matches_subterm_vect : t -> constr -> context * constr array := + "ltac2" "pattern_matches_subterm_vect". +(** Internal version of [matches_subterms] that does not return the identifiers. *) + Ltac2 @ external instantiate : context -> constr -> constr := "ltac2" "pattern_instantiate". (** Fill the hole of a context with the given term. *) |