diff options
| author | Pierre-Marie Pédrot | 2020-12-12 14:39:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:46:45 +0100 |
| commit | 421ed6bb43e01a2675df2cfae286d1cfcc691fcc (patch) | |
| tree | 3bc425e990ecb93f1a9ac5e428466ef75cf1fd1e /tactics/redexpr.mli | |
| parent | 12d53dc64fa565ae6408d2ebb668e997b7e574b3 (diff) | |
Small API encapsulation inside Redexpr.
We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.
Diffstat (limited to 'tactics/redexpr.mli')
| -rw-r--r-- | tactics/redexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index 8350a831ca..5f3a7b689b 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -21,14 +21,14 @@ open Locus type red_expr = (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 +type red_expr_val 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 +val reduction_of_red_expr_val : ?occs:(Locus.occurrences_expr * int) -> + red_expr_val -> e_reduction_function * cast_kind (** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *) val reduction_of_red_expr : |