diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 23 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 16 |
3 files changed, 27 insertions, 18 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index f3c7680b01..0a9182e0b9 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -344,8 +344,21 @@ let intern_typed_pattern ist p = (* type it, so we remember the pattern as a glob_constr only *) (intern_constr_gen true false ist p,dummy_pat) -let intern_typed_pattern_with_occurrences ist (l,p) = - (l,intern_typed_pattern ist p) +let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = + match p with + | Inl r -> l, + (try Inl (intern_evaluable ist r) + with e when Logic.catchable_exception e -> + (* Compatibility. In practice, this means that the code above + is useless. Still the idea of having either an evaluable + ref or a pattern seems interesting, with "head" reduction + in case of an evaluable ref, and "strong" reduction in the + subterm matched when a pattern) *) + let r = match r with + | AN r -> r + | _ -> Qualid (loc_of_smart_reference r,qualid_of_path (path_of_global (smart_global r))) in + Inr (intern_typed_pattern ist (CRef(r,None)))) + | Inr c -> l, Inr (intern_typed_pattern ist c) (* This seems fairly hacky, but it's the first way I've found to get proper globalization of [unfold]. --adamc *) @@ -370,9 +383,9 @@ let intern_red_expr ist = function | Cbn f -> Cbn (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) - | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o) - | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o) - | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o) + | Simpl o -> Simpl (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r let intern_in_hyp_as ist lf (clear,id,ipat) = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 54fbbbe274..63eb200de8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -680,8 +680,10 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let (sigma,c_interp) = interp_constr ist env sigma c in sigma , (interp_occurrences ist occs, c_interp) -let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, c) = - let _, p = interp_typed_pattern ist env sigma c in +let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = + let p = match a with + | Inl b -> Inl (interp_evaluable ist env sigma b) + | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 2f47b90002..5a02a53f3e 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -114,17 +114,11 @@ let subst_glob_constr_or_pattern subst (c,p) = let subst_pattern_with_occurrences subst (l,p) = (l,subst_glob_constr_or_pattern subst p) -let subst_redexp subst = function - | Unfold l -> Unfold (List.map (subst_unfold subst) l) - | Fold l -> Fold (List.map (subst_glob_constr subst) l) - | Cbv f -> Cbv (subst_flag subst f) - | Cbn f -> Cbn (subst_flag subst f) - | Lazy f -> Lazy (subst_flag subst f) - | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) - | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o) - | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o) - | CbvNative o -> CbvNative (Option.map (subst_pattern_with_occurrences subst) o) - | (Red _ | Hnf | ExtraRedExpr _ as r) -> r +let subst_redexp subst = + Miscops.map_red_expr_gen + (subst_glob_constr subst) + (subst_evaluable subst) + (subst_glob_constr_or_pattern subst) let subst_raw_may_eval subst = function | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c) |