diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 16:59:27 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-17 11:52:38 +0100 |
commit | 653de32139ecee3114779a5ee2961c58793889e5 (patch) | |
tree | 5afe95bfaa5af025f92e9aea27147862487c0fb0 /plugins/ltac/tactic_matching.mli | |
parent | bcb634d070519d6e37d9b7d39f12437a7d38f0c2 (diff) |
Ltac as a plugin.
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
Diffstat (limited to 'plugins/ltac/tactic_matching.mli')
-rw-r--r-- | plugins/ltac/tactic_matching.mli | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli new file mode 100644 index 000000000..090207bcc --- /dev/null +++ b/plugins/ltac/tactic_matching.mli @@ -0,0 +1,49 @@ + (************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This file extends Matching with the main logic for Ltac's + (lazy)match and (lazy)match goal. *) + + +(** [t] is the type of matching successes. It ultimately contains a + {!Tacexpr.glob_tactic_expr} representing the left-hand side of the + corresponding matching rule, a matching substitution to be + applied, a context substitution mapping identifier to context like + those of {!Matching.matching_result}), and a {!Term.constr} + substitution mapping corresponding to matched hypotheses. *) +type 'a t = { + subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + context : Term.constr Names.Id.Map.t; + terms : Term.constr Names.Id.Map.t; + lhs : 'a; +} + + +(** [match_term env sigma term rules] matches the term [term] with the + set of matching rules [rules]. The environment [env] and the + evar_map [sigma] are not currently used, but avoid code + duplication. *) +val match_term : + Environ.env -> + Evd.evar_map -> + Term.constr -> + (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + Tacexpr.glob_tactic_expr t Proofview.tactic + +(** [match_goal env sigma hyps concl rules] matches the goal + [hyps|-concl] with the set of matching rules [rules]. The + environment [env] and the evar_map [sigma] are used to check + convertibility for pattern variables shared between hypothesis + patterns or the conclusion pattern. *) +val match_goal: + Environ.env -> + Evd.evar_map -> + Context.Named.t -> + Term.constr -> + (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + Tacexpr.glob_tactic_expr t Proofview.tactic |