From 421ed6bb43e01a2675df2cfae286d1cfcc691fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Dec 2020 14:39:18 +0100
Subject: 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.
---
 tactics/redexpr.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics/redexpr.mli')

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