diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 59cd065d..afffaffb 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x -let subst_glob_constr_and_expr subst (c,e) = - assert (Option.is_empty e); (* e<>None only for toplevel tactics *) - (Detyping.subst_glob_constr subst c,None) +let subst_glob_constr_and_expr subst (c, e) = + (Detyping.subst_glob_constr subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) @@ -100,20 +99,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) |