diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 1 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
3 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9a4995c03a..a76402e096 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -309,6 +309,7 @@ GEXTEND Gram | IDENT "assumption" -> TacAssumption | IDENT "exact"; c = constr -> TacExact c | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c + | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c | IDENT "apply"; cl = constr_with_bindings -> TacApply cl | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index ebf4b5ad1c..4956345120 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -652,6 +652,7 @@ and pr_atom1 = function | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) + | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) | TacElim (cb,cbo) -> hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 70bc3f6822..56dd32c555 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -271,6 +271,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> | Tacexpr.TacExactNoCheck c -> <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacVmCastNoCheck c -> + <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply cb -> <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (cb,cbo) -> |