diff options
| author | Pierre-Marie Pédrot | 2017-10-25 12:13:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-27 11:48:40 +0200 |
| commit | d4172d2c7a48d932b42248fe57c6c2a87ac57e30 (patch) | |
| tree | 48f49fa0490659f3f505f26ef6fb86d6ae0eae64 /src/tac2qexpr.mli | |
| parent | 0b26bfc8e068e1e95eeea9db0c3bda7436ac8338 (diff) | |
Stubs for goal matching: quotation and matching function.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 21 |
1 files changed, 17 insertions, 4 deletions
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 |