From 98da9fdce866728f93bc7cb690275f5559aa9bae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Apr 2017 20:37:15 +0200 Subject: Removing various tactic compatibility layers in core tactics. --- plugins/ltac/g_class.ml4 | 2 +- plugins/ltac/g_rewrite.ml4 | 13 +++++++++---- plugins/ltac/rewrite.ml | 6 +++--- 3 files changed, 13 insertions(+), 8 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 40f30c7943..ff5e7d5ff2 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -85,7 +85,7 @@ TACTIC EXTEND not_evar END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] + [ "is_ground" constr(ty) ] -> [ is_ground ty ] END TACTIC EXTEND autoapply diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c50100bf55..fdcaedab3a 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -19,6 +19,7 @@ open Geninterp open Extraargs open Tacmach open Tacticals +open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = + Proofview.Goal.enter { enter = begin fun gl -> let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in - Tacticals.onAllHypsAndConcl + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun cl -> match cl with - | Some id when is_tac id -> tclIDTAC - | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl)) + | Some id when is_tac id -> Tacticals.New.tclIDTAC + | _ -> cl_rewrite_clause c o AllOccurrences cl) + (None :: List.map (fun id -> Some id) hyps) + end } TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ] +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b84be4600c..12a1566e20 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2197,7 +2197,8 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - Proofview.V82.tactic (fun gl -> + let open Tacmach.New in + Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2211,11 +2212,10 @@ let setoid_symmetry_in id = let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - Proofview.V82.of_tactic (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - gl) + end } let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry -- cgit v1.2.3 From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 19:12:49 -0400 Subject: Add transparent_abstract tactic --- plugins/ltac/extratactics.ml4 | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb7599..a96623a5f6 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -815,6 +815,19 @@ TACTIC EXTEND destauto | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END +(**********************************************************************) + +(**********************************************************************) +(* A version of abstract constructing transparent terms *) +(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) +(**********************************************************************) + +TACTIC EXTEND transparent_abstract +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ] +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ] +END (* ********************************************************************* *) -- cgit v1.2.3 From 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:29:35 +0200 Subject: Remove unused [rec] keywords --- plugins/ltac/pptactic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 39ae1f41d2..b73b66e56f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -250,7 +250,7 @@ type 'a extra_genarg_printer = let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in - let rec pr = function + let pr = function | TacTerm s -> primitive s | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) in @@ -314,7 +314,7 @@ type 'a extra_genarg_printer = | Extend.Uentry _ | Extend.Uentryl _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" - let rec pr_targ prtac symb arg = match symb with + let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> prtac (1, Any) arg | Extend.Uentryl (_, l) -> prtac (l, Any) arg -- cgit v1.2.3 From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- plugins/ltac/tacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index cd8c9e471e..8cda73b4bf 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -320,7 +320,7 @@ let add_tactic_notation local n prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local n prods false ids tac + add_glob_tactic_notation local ~level:n prods false ids tac (**********************************************************************) (* ML Tactic entries *) -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- plugins/ltac/extratactics.ml4 | 2 -- plugins/ltac/profile_ltac.ml | 1 - plugins/ltac/tacentries.ml | 3 --- plugins/ltac/tacintern.ml | 6 ------ plugins/ltac/tacinterp.ml | 6 ------ 5 files changed, 18 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 38fdfb7599..35cfe8b542 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -52,8 +52,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac = let replace_term ist dir_opt c cl = with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) -let clause = Pltac.clause_dft_concl - TACTIC EXTEND replace ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index bcb28f77ce..a853576f25 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -136,7 +136,6 @@ let feedback_results results = let format_sec x = (Printf.sprintf "%.3fs" x) let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) let padl n s = ws (max 0 (n - utf8_length s)) ++ str s -let padr n s = str s ++ ws (max 0 (n - utf8_length s)) let padr_with c n s = let ulength = utf8_length s in str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 8cda73b4bf..ef1d69d35b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -88,9 +88,6 @@ let rec parse_user_entry s sep = else Uentry s -let arg_list = function Rawwit t -> Rawwit (ListArg t) -let arg_opt = function Rawwit t -> Rawwit (OptArg t) - let interp_entry_name interp symb = let rec eval = function | Ulist1 e -> Ulist1 (eval e) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e9..75227def0f 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function GRef (loc,locate_global_with_alias lqid,None), if strict then None else Some (CRef (r,None)) -let intern_move_location ist = function - | MoveAfter id -> MoveAfter (intern_hyp ist id) - | MoveBefore id -> MoveBefore (intern_hyp ist id) - | MoveFirst -> MoveFirst - | MoveLast -> MoveLast - (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 50f43931e9..fcdf7bb2cd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -436,12 +436,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) = let interp_hyp_list ist env sigma l = List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l) -let interp_move_location ist env sigma = function - | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id) - | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id) - | MoveFirst -> MoveFirst - | MoveLast -> MoveLast - let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar (loc, id) -> -- cgit v1.2.3 From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:07:32 +0200 Subject: Add [_] prefix to unused values which maybe should be kept --- plugins/ltac/tauto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index dc7ee6a234..e86d1c7283 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -242,7 +242,7 @@ let tauto_uniform_unit_flags = { } (* This is the compatibility mode (not used) *) -let tauto_legacy_flags = { +let _tauto_legacy_flags = { binary_mode = true; binary_mode_bugged_detection = true; strict_in_contravariant_hyp = true; -- cgit v1.2.3 From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- plugins/ltac/evar_tactics.ml | 1 - plugins/ltac/extratactics.ml4 | 1 - plugins/ltac/g_auto.ml4 | 1 - plugins/ltac/g_class.ml4 | 3 --- plugins/ltac/pltac.ml | 1 - plugins/ltac/rewrite.mli | 1 - plugins/ltac/taccoerce.mli | 1 - plugins/ltac/tacentries.ml | 1 - plugins/ltac/tacenv.mli | 1 - plugins/ltac/tacinterp.ml | 1 - plugins/ltac/tacinterp.mli | 1 - plugins/ltac/tactic_debug.mli | 1 - 12 files changed, 14 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 5d3f6df03d..bc9c300e23 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -9,7 +9,6 @@ open Util open Names open Term -open EConstr open CErrors open Evar_refiner open Tacmach diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 35cfe8b542..21419d1f92 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -21,7 +21,6 @@ open Tacexpr open Glob_ops open CErrors open Util -open Evd open Termops open Equality open Misctypes diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index dfa8331ff2..50e8255a67 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -16,7 +16,6 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr -open Proofview.Notations open Names DECLARE PLUGIN "g_auto" diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index ff5e7d5ff2..23ce368eea 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,9 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Misctypes open Class_tactics -open Pltac open Stdarg open Tacarg open Names @@ -95,7 +93,6 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) open Term -open Proofview.Goal open Proofview.Notations let rec eq_constr_mod_evars sigma x y = diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 1d21118ae8..7e979d269d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 7a20838a27..6683d753bc 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -14,7 +14,6 @@ open Constrexpr open Tacexpr open Misctypes open Evd -open Proof_type open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 9c4ac52657..4a44f86d92 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -8,7 +8,6 @@ open Util open Names -open Term open EConstr open Misctypes open Pattern diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ef1d69d35b..32750383b8 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -15,7 +15,6 @@ open Genarg open Extend open Pcoq open Egramml -open Egramcoq open Vernacexpr open Libnames open Nameops diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 94e14223aa..d1e2a7bbe6 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Genarg open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fcdf7bb2cd..b8c021f188 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -25,7 +25,6 @@ open Refiner open Tacmach.New open Tactic_debug open Constrexpr -open Term open Termops open Tacexpr open Genarg diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 1e5f6bd42b..494f36a95a 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -8,7 +8,6 @@ open Names open Tactic_debug -open Term open EConstr open Tacexpr open Genarg diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 7745d9b7b6..0b4d35a22a 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -10,7 +10,6 @@ open Environ open Pattern open Names open Tacexpr -open Term open EConstr open Evd -- cgit v1.2.3 From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:31:15 +0200 Subject: Fix 4.04 warnings --- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/tauto.ml | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 12a1566e20..9a1615d3f2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -39,7 +39,7 @@ open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) (** Typeclass-based generalized rewriting. *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index e86d1c7283..4de2081cf8 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -10,7 +10,6 @@ open Term open EConstr open Hipattern open Names -open Pp open Geninterp open Misctypes open Tacexpr -- cgit v1.2.3 From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 27 Apr 2017 21:58:52 +0200 Subject: Post-rebase warnings (unused opens and 2 unused values) --- plugins/ltac/g_rewrite.ml4 | 1 - plugins/ltac/rewrite.ml | 1 - 2 files changed, 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index fdcaedab3a..ac979bcf89 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -18,7 +18,6 @@ open Glob_term open Geninterp open Extraargs open Tacmach -open Tacticals open Proofview.Notations open Rewrite open Stdarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9a1615d3f2..5630a2d7b6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -17,7 +17,6 @@ open EConstr open Vars open Reduction open Tacticals.New -open Tacmach open Tactics open Pretype_errors open Typeclasses -- cgit v1.2.3 From 8f4d79115c3686de41e20c41ef6dbce8b8546366 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Feb 2017 18:51:36 +0100 Subject: Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in batch mode. --- plugins/ltac/tactic_debug.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index dffeade298..dac15ff79e 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None) +let batch = ref false + +open Goptions + +let _ = + declare_bool_option + { optsync = false; + optdepr = false; + optname = "Ltac batch debug"; + optkey = ["Ltac";"Batch";"Debug"]; + optread = (fun () -> !batch); + optwrite = (fun x -> batch := x) } + let rec drop_spaces inst i = if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) else i @@ -150,6 +163,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + if Pervasives.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with -- cgit v1.2.3 From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 May 2017 22:30:09 +0200 Subject: Adding support for using grammar entries returning no value in EXTEND. --- plugins/ltac/g_ltac.ml4 | 8 ++++++-- plugins/ltac/pptactic.ml | 7 ++++--- plugins/ltac/pptactic.mli | 2 +- plugins/ltac/tacentries.ml | 14 +++++++------- plugins/ltac/tacentries.mli | 2 +- 5 files changed, 19 insertions(+), 14 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ca5d198c23..d717ed0a53 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -460,7 +460,9 @@ END let pr_ltac_production_item = function | Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, (arg, sep), id) -> +| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg +| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false +| Tacentries.TacNonTerm (_, (arg, sep), Some id) -> let sep = match sep with | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) @@ -470,7 +472,9 @@ let pr_ltac_production_item = function VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ] + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ] +| [ ident(nt) ] -> + [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ] END VERNAC COMMAND EXTEND VernacTacticNotation diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b73b66e56f..a619575591 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list @@ -264,8 +264,9 @@ type 'a extra_genarg_printer = let rec pack prods args = match prods, args with | [], [] -> [] | TacTerm s :: prods, args -> TacTerm s :: pack prods args - | TacNonTerm (loc, symb, id) :: prods, arg :: args -> - TacNonTerm (loc, (symb, arg), id) :: pack prods args + | TacNonTerm (_, _, None) :: prods, args -> pack prods args + | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), ido) :: pack prods args | _ -> raise Not_found in let prods = pack pp.pptac_prods l in diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 729338fb9a..433f342c4f 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -21,7 +21,7 @@ open Ppextend type 'a grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 32750383b8..91262f6fd6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -21,7 +21,7 @@ open Nameops type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option type argument = Genarg.ArgT.any Extend.user_symbol @@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state = in let map = function | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> + | TacNonTerm (loc, s, ido) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, typ, e) + GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in @@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), id) -> + | TacNonTerm (loc, (nt, sep), ido) -> let symbol = parse_user_entry nt sep in let interp s = function | None -> @@ -220,7 +220,7 @@ let interp_prod_item = function end in let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) + TacNonTerm (loc, symbol, ido) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj = let cons_production_parameter = function | TacTerm _ -> None -| TacNonTerm (_, _, id) -> Some id +| TacNonTerm (_, _, ido) -> ido let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { @@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods = let open Tacexpr in let get_id = function | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id + | TacNonTerm (_, _, ido) -> ido in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 0695044736..dac62dad33 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr = | TacTerm of string -| TacNonTerm of Loc.t * 'a * Names.Id.t +| TacNonTerm of Loc.t * 'a * Names.Id.t option type raw_argument = string * string option (** An argument type as provided in Tactic notations, i.e. a string like -- cgit v1.2.3 From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 May 2017 22:31:08 +0200 Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. --- plugins/ltac/extraargs.ml4 | 20 ++++++++++++++++++++ plugins/ltac/extraargs.mli | 4 ++++ plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/g_tactic.ml4 | 13 +------------ 4 files changed, 26 insertions(+), 13 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 53b726432c..ec3a49df49 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause | [ in_clause'(cl) ] -> [ cl ] END +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon +| [ local_test_lpar_id_colon(x) ] -> [ () ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7d4bccfadd..9b41675120 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,6 +67,10 @@ val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> raw_tactic_expr option -> Pp.std_ppcmds +val test_lpar_id_colon : unit Pcoq.Gram.entry + +val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type + (** Spiwack: Primitive for retroknowledge registration *) val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 3e6ccaf84a..bd48614dbc 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -463,7 +463,7 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 4b3ca80af5..e33c25cf88 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq = | _ -> err ()) (* idem for (x:t) *) -let test_lpar_id_colon = - Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) +open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = -- cgit v1.2.3