diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 59cd065d12..42e61cb57e 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -100,20 +100,11 @@ let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in subst_or_var (subst_and_short_name subst_eval_ref) -let subst_unfold subst (l,e) = - (l,subst_evaluable subst e) - -let subst_flag subst red = - { red with rConst = List.map (subst_evaluable subst) red.rConst } - let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (c,p) = (subst_glob_constr subst c,subst_pattern subst p) -let subst_pattern_with_occurrences subst (l,p) = - (l,subst_glob_constr_or_pattern subst p) - let subst_redexp subst = Miscops.map_red_expr_gen (subst_glob_constr subst) |