diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6f459b15c..00dc19332 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -552,7 +552,7 @@ let intern_redexp ist = function | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o) - | (Red _ | Hnf as r) -> r + | (Red _ | Hnf | CbvVm as r ) -> r | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c) let intern_inversion_strength lf ist = function @@ -637,6 +637,7 @@ let rec intern_atomic lf ist x = option_app (intern_hyp ist) ido') | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) + | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) | TacApply cb -> TacApply (intern_constr_with_bindings ist cb) | TacElim (cb,cbo) -> TacElim (intern_constr_with_bindings ist cb, @@ -1233,7 +1234,7 @@ let redexp_interp ist sigma env = function | Lazy f -> Lazy (interp_flag ist env f) | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o) - | (Red _ | Hnf as r) -> r + | (Red _ | Hnf | CbvVm as r) -> r | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c) let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl) @@ -1653,6 +1654,7 @@ and interp_atomic ist gl = function (option_app (interp_hyp ist gl) ido') | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) + | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb) | TacElim (cb,cbo) -> h_elim (interp_constr_with_bindings ist gl cb) @@ -1894,7 +1896,7 @@ let subst_redexp subst = function | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o) - | (Red _ | Hnf as r) -> r + | (Red _ | Hnf | CbvVm as r) -> r | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c) let subst_raw_may_eval subst = function @@ -1918,6 +1920,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x | TacAssumption as x -> x | TacExact c -> TacExact (subst_rawconstr subst c) + | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) | TacApply cb -> TacApply (subst_raw_with_bindings subst cb) | TacElim (cb,cbo) -> TacElim (subst_raw_with_bindings subst cb, |