diff options
| author | Pierre-Marie Pédrot | 2020-12-10 17:37:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:35:15 +0100 |
| commit | 35ead413491cb0297dff4458d4a891cdc607b0d9 (patch) | |
| tree | abd222d5c6e7a99115c407644145ab1f91897ea5 /tactics/redexpr.mli | |
| parent | b7ec355d3af240519cde9660dd2562b93f87c555 (diff) | |
Split the intepretation of red_exprs in two phases.
Diffstat (limited to 'tactics/redexpr.mli')
| -rw-r--r-- | tactics/redexpr.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index d43785218f..8350a831ca 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -19,10 +19,18 @@ open Reductionops open Locus type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen + (constr, evaluable_global_reference, constr_pattern) red_expr_gen + +type red_expr_val = + (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a +val eval_red_expr : Environ.env -> red_expr -> red_expr_val + +val reduction_of_red_expr_val : red_expr_val -> e_reduction_function * cast_kind + +(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *) val reduction_of_red_expr : Environ.env -> red_expr -> e_reduction_function * cast_kind |