diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-30 18:17:13 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-30 18:17:13 +0000 |
| commit | f1c54f39609fd2e13fb339a6a94f9f500f7af3a5 (patch) | |
| tree | 9ccb296cce573b392bd6e33d7fa6fcbc70fed615 /tactics/tacinterp.ml | |
| parent | 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850 (diff) | |
Added an pattern / occurence syntax for vm_compute.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index fecc2bac1..e2a99707f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -569,7 +569,8 @@ let intern_red_expr ist = function | 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) - | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r + | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o) + | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r let intern_in_hyp_as ist lf (id,ipat) = (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat) @@ -1365,8 +1366,10 @@ let interp_red_expr ist sigma env = function | Pattern l -> Pattern (List.map (interp_constr_with_occurrences ist env sigma) l) | Simpl o -> - Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) - | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r + Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | CbvVm o -> + CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -2593,7 +2596,8 @@ let subst_redexp subst = function | 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) - | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r + | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o) + | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let subst_raw_may_eval subst = function | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c) |