diff options
| author | Pierre-Marie Pédrot | 2014-05-18 02:50:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 14:49:47 +0200 |
| commit | e705ae9d343c67212ce238899d21059ce93ee3e5 (patch) | |
| tree | 33eb5575b2da7275fdb13295243ef045afab3375 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/pptactic.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c7644f8c60..0ea8b4048c 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -650,8 +650,6 @@ and pr_atom1 = function hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscprint.pr_move_location pr_ident hto) | 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 (a,ev,cb,inhyp) -> hov 1 ((if a then mt() else str "simple ") ++ str (with_evars ev "apply") ++ spc () ++ @@ -660,10 +658,8 @@ and pr_atom1 = function | TacElim (ev,cb,cbo) -> hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) - | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c) | TacCase (ev,cb) -> hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb) - | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ @@ -672,7 +668,6 @@ and pr_atom1 = function | TacMutualCofix (id,l) -> hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc pr_cofix_tac l) - | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c) | TacAssert (Some tac,ipat,c) -> hov 1 (str "assert" ++ pr_assumption pr_lconstr pr_constr ipat c ++ @@ -734,8 +729,6 @@ and pr_atom1 = function | TacSpecialize (n,c) -> hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ pr_with_bindings c) - | TacLApply c -> - hov 1 (str "lapply" ++ pr_constrarg c) (* Automation tactics *) | TacTrivial (_,[],Some []) as x -> pr_atom0 x |