diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index e17db58c63..df3a0b9736 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -7,6 +7,7 @@ open Term open Environ open Evd open Reduction +open Closure (*i*) (*s Reduction functions associated to tactics. \label{tacred} *) @@ -23,7 +24,8 @@ val hnf_constr : 'a reduction_function val nf : 'a reduction_function (* Unfold *) -val unfoldn : (int list * section_path) list -> 'a reduction_function +val unfoldn : + (int list * evaluable_global_reference) list -> 'a reduction_function (* Fold *) val fold_commands : constr list -> 'a reduction_function @@ -53,7 +55,7 @@ type red_expr = | Simpl | Cbv of Closure.flags | Lazy of Closure.flags - | Unfold of (int list * section_path) list + | Unfold of (int list * evaluable_global_reference) list | Fold of constr list | Pattern of (int list * constr * constr) list |