From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- tactics/tacsubst.ml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) (limited to 'tactics/tacsubst.ml') 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) -- cgit v1.2.3