From d4172d2c7a48d932b42248fe57c6c2a87ac57e30 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 25 Oct 2017 12:13:27 +0200
Subject: Stubs for goal matching: quotation and matching function.

---
 src/tac2qexpr.mli | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index cb43a980de..229cece7c4 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -118,14 +118,27 @@ type red_flag = red_flag_r located
 
 type strategy_flag = red_flag list located
 
-type constr_match_branch_r =
-| QConstrMatchPattern of Constrexpr.constr_expr * raw_tacexpr
-| QConstrMatchContext of Id.t option * Constrexpr.constr_expr * raw_tacexpr
+type constr_match_pattern_r =
+| QConstrMatchPattern of Constrexpr.constr_expr
+| QConstrMatchContext of Id.t option * Constrexpr.constr_expr
 
-type constr_match_branch = constr_match_branch_r located
+type constr_match_pattern = constr_match_pattern_r located
+
+type constr_match_branch = (constr_match_pattern * raw_tacexpr) located
 
 type constr_matching = constr_match_branch list located
 
+type goal_match_pattern_r = {
+  q_goal_match_concl : constr_match_pattern;
+  q_goal_match_hyps : (Name.t located * constr_match_pattern) list;
+}
+
+type goal_match_pattern = goal_match_pattern_r located
+
+type goal_match_branch = (goal_match_pattern * raw_tacexpr) located
+
+type goal_matching = goal_match_branch list located
+
 type hintdb_r =
 | QHintAll
 | QHintDbs of Id.t located or_anti list
-- 
cgit v1.2.3