From 6150d15647afc739329019f7e9de595187ecc282 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 16:08:50 +0200 Subject: Removing the Entry module now that rules need not be marshalled. --- ltac/tacentries.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 881482081a..d0383ffbcb 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -43,8 +43,8 @@ let coincide s pat off = !break let atactic n = - if n = 5 then Aentry (name_of_entry Tactic.binder_tactic) - else Aentryl (name_of_entry Tactic.tactic_expr, n) + if n = 5 then Aentry Tactic.binder_tactic + else Aentryl (Tactic.tactic_expr, n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name @@ -149,7 +149,7 @@ let rec prod_item_of_symbol lev = function | Extend.Uentry arg -> let ArgT.Any tag = arg in let wit = ExtraArg tag in - EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit))) + EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in assert (coincide (ArgT.repr tag) "tactic" 0); @@ -389,8 +389,8 @@ let create_ltac_quotation name cast (e, l) = in let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with - | None -> Aentry (name_of_entry e) - | Some l -> Aentryl (name_of_entry e, l) + | None -> Aentry e + | Some l -> Aentryl (e, l) in (* let level = Some "1" in *) let level = None in -- cgit v1.2.3 From 61f79019be6082c3ebabd503c322fb2edb05a99a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 11:11:39 +0200 Subject: AlistNsep token now accepts an arbitrary separator. --- ltac/tacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index d0383ffbcb..f829ae4f57 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -139,10 +139,10 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit (ListArg typ), Alist0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in EntryName (Rawwit (OptArg typ), Aopt e) -- cgit v1.2.3 From 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 10:30:49 +0200 Subject: Moving the grammar summary to Pcoq. --- ltac/tacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f829ae4f57..5c1e7c0330 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) = let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn) +let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn) (**********************************************************************) (* Tactic Notation *) -- cgit v1.2.3 From df2d71323081f8a395881ffc0e1793e429abc3bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 11:28:04 +0200 Subject: Turning the grammar extend command API into a state-passing one. --- ltac/tacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 5c1e7c0330..aedcb76eb7 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -157,7 +157,7 @@ let rec prod_item_of_symbol lev = function (** Tactic grammar extensions *) -let add_tactic_entry (kn, ml, tg) = +let add_tactic_entry (kn, ml, tg) state = let open Tacexpr in let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = @@ -186,7 +186,7 @@ let add_tactic_entry (kn, ml, tg) = let rules = make_rule mkact prods in synchronize_level_positions (); grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - 1 + (1, state) let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -- cgit v1.2.3 From 85753a0bdb6183604a78232c4c32fd15f7a21a2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 13:25:02 +0200 Subject: Moving the constr empty entry registering to the state-based API. --- ltac/tacentries.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index aedcb76eb7..714bfa8417 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -184,7 +184,6 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - synchronize_level_positions (); grammar_extend entry None (pos, [(None, None, List.rev [rules])]); (1, state) -- cgit v1.2.3 From 16d0e6f7cfc453944874cc1665a0eb4db8ded354 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 15:33:47 +0200 Subject: Making the grammar command extend API purely functional. Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function. --- ltac/tacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac/tacentries.ml') diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 714bfa8417..5720a6f378 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -184,8 +184,8 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - (1, state) + let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + ([r], state) let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -- cgit v1.2.3