From 48327426b59144f1a7181092068077c5a6df7c60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:45:31 +0100 Subject: Moving the "fix" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 12667d0f24..fe0be9b255 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -828,7 +828,6 @@ module Make ++ pr_opt pr_eliminator cbo) | TacCase (ev,cb) -> hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() -- cgit v1.2.3 From bda8b2e8f90235ca875422f211cb781068b20b3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:54:08 +0100 Subject: Moving the "cofix" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fe0be9b255..05c3b3bf42 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -832,8 +832,6 @@ module Make hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 ( primitive "cofix" ++ spc () ++ pr_id id ++ spc() -- cgit v1.2.3 From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:05:26 +0100 Subject: Moving the "clear" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 9 --------- 1 file changed, 9 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 05c3b3bf42..c61b80c834 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -793,7 +793,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -899,14 +898,6 @@ module Make ) (* Context management *) - | TacClear (true,[]) as t -> - pr_atom0 t - | TacClear (keep,l) -> - hov 1 ( - primitive "clear" ++ spc () - ++ (if keep then str "- " else mt ()) - ++ prlist_with_sep spc pr.pr_name l - ) | TacClearBody l -> hov 1 ( primitive "clearbody" ++ spc () -- cgit v1.2.3 From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:20:26 +0100 Subject: Moving the "clearbody" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c61b80c834..b1d6fb0c0f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -898,11 +898,6 @@ module Make ) (* Context management *) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) | TacMove (id1,id2) -> hov 1 ( primitive "move" -- cgit v1.2.3 From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:35:34 +0100 Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b1d6fb0c0f..f4007e25e1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -854,11 +854,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> -- cgit v1.2.3 From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:11:52 +0100 Subject: Moving the "symmetry" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f4007e25e1..689ac6e4eb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -935,10 +935,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( -- cgit v1.2.3 From 293222e49ff81bc1299b3822d2a8c526ca803307 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:40:45 +0100 Subject: Moving the "exists" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 689ac6e4eb..2c57cb811e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -725,7 +725,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -909,13 +908,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( -- cgit v1.2.3 From 1397f791b1699b0f04d971465270d5b2df9a6d7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 13:32:39 +0100 Subject: Moving the "move" tactic to TACTIC EXTEND. --- printing/pptactic.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'printing') diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2c57cb811e..36863906ea 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -892,12 +892,6 @@ module Make ) (* Context management *) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) | TacRename l -> hov 1 ( primitive "rename" ++ brk (1,1) -- cgit v1.2.3