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. --- parsing/g_tactic.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 77b7b05a39..497819b327 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -555,8 +555,6 @@ GEXTEND Gram TacAtom (!@loc, TacElim (true,cl,el)) | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl) | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) - | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n)) - | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n)) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) | "cofix" -> TacAtom (!@loc, TacCofix None) -- 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. --- parsing/g_tactic.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 497819b327..6c3918be3a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -557,8 +557,6 @@ GEXTEND Gram | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) - | "cofix" -> TacAtom (!@loc, TacCofix None) - | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id)) | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd)) -- 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. --- parsing/g_tactic.ml4 | 4 ---- 1 file changed, 4 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 6c3918be3a..ad5f78b46d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -618,10 +618,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l)) - | IDENT "clear"; l = LIST0 id_or_meta -> - let is_empty = match l with [] -> true | _ -> false in - TacAtom (!@loc, TacClear (is_empty, l)) | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l) | IDENT "move"; hfrom = id_or_meta; hto = move_location -> TacAtom (!@loc, TacMove (hfrom,hto)) -- 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. --- parsing/g_tactic.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ad5f78b46d..04ee02f944 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -618,7 +618,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l) | IDENT "move"; hfrom = id_or_meta; hto = move_location -> TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) -- 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. --- parsing/g_tactic.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 04ee02f944..238b9a60f7 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -603,7 +603,6 @@ GEXTEND Gram na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) - | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c) (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> -- 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. --- parsing/g_tactic.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 238b9a60f7..4587e321f0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -625,8 +625,6 @@ GEXTEND Gram | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) | IDENT "eexists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (true,bll)) - (* Equivalence relations *) - | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl) (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; -- 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. --- parsing/g_tactic.ml4 | 5 ----- 1 file changed, 5 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4587e321f0..e50eca25be 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -621,11 +621,6 @@ GEXTEND Gram TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) - (* Constructors *) - | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) - | IDENT "eexists"; bll = opt_bindings -> - TacAtom (!@loc, TacSplit (true,bll)) - (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) -- 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. --- parsing/g_tactic.ml4 | 2 -- 1 file changed, 2 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index e50eca25be..0c90a8bca4 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -617,8 +617,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "move"; hfrom = id_or_meta; hto = move_location -> - TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) (* Equality and inversion *) -- cgit v1.2.3