diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-18 02:50:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-20 14:49:47 +0200 |
| commit | e705ae9d343c67212ce238899d21059ce93ee3e5 (patch) | |
| tree | 33eb5575b2da7275fdb13295243ef045afab3375 /grammar/q_coqast.ml4 | |
| parent | f79e9db4922f649d08153f09526d5c1c60a7e45c (diff) | |
Tentative to add constr-using primitive tactics without grammar rules.
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
Diffstat (limited to 'grammar/q_coqast.ml4')
| -rw-r--r-- | grammar/q_coqast.ml4 | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index abc0d31a9..6a413ca31 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -310,23 +310,15 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> | Tacexpr.TacExact c -> <: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 (b,false,cb,None) -> <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> - | Tacexpr.TacElimType c -> - <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> | Tacexpr.TacCase (false,cb) -> let cb = mlexpr_of_constr_with_binding cb in <:expr< Tacexpr.TacCase False $cb$ >> - | Tacexpr.TacCaseType c -> - <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >> | Tacexpr.TacFix (ido,n) -> let ido = mlexpr_of_ident_option ido in let n = mlexpr_of_int n in @@ -346,8 +338,6 @@ let rec mlexpr_of_atomic_tactic = function let l = mlexpr_of_list f l in <:expr< Tacexpr.TacMutualCofix $id$ $l$ >> - | Tacexpr.TacCut c -> - <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ |