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/genredexpr.ml | |
| 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/genredexpr.ml')
| -rw-r--r-- | tactics/genredexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml index 9939490e79..a9100efddb 100644 --- a/tactics/genredexpr.ml +++ b/tactics/genredexpr.ml @@ -76,7 +76,7 @@ type 'a and_short_name = 'a * Names.lident option let wit_red_expr : ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen, - (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen) + (Genintern.glob_constr_and_expr,Tacred.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen, + (EConstr.t,Tacred.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen) Genarg.genarg_type = make0 "redexpr" |