diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /tactics/tacsubst.ml | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
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) |