From 653de32139ecee3114779a5ee2961c58793889e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 6 Oct 2016 16:59:27 +0200
Subject: 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.
---
 plugins/ltac/tactic_matching.mli | 49 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 plugins/ltac/tactic_matching.mli

(limited to 'plugins/ltac/tactic_matching.mli')

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
-- 
cgit v1.2.3