diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /tactics/redexpr.mli | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'tactics/redexpr.mli')
| -rw-r--r-- | tactics/redexpr.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index 5f3a7b689b..fb0043db8d 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -10,7 +10,6 @@ (** Interpretation layer of redexprs such as hnf, cbv, etc. *) -open Names open Constr open EConstr open Pattern @@ -19,7 +18,7 @@ open Reductionops open Locus type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen + (constr, Tacred.evaluable_global_reference, constr_pattern) red_expr_gen type red_expr_val @@ -50,7 +49,7 @@ val declare_red_expr : bool -> string -> red_expr -> unit true, the effect is non-synchronous (i.e. it does not survive section and module closure). *) val set_strategy : - bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit + bool -> (Conv_oracle.level * Tacred.evaluable_global_reference list) list -> unit (** call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function |