diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-06 20:16:32 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-07 15:42:49 +0200 |
commit | 5520db62486ad628f91737833623aa69c4c1b8af (patch) | |
tree | 854f2dd80c0c1b0d1167996f452f507a9ecececa /parsing | |
parent | 33f7d95a655add1967b5c520eb05e816963e1936 (diff) |
Removing the use to Egramcoq.recover_constr_grammar.
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/egramcoq.ml | 27 | ||||
-rw-r--r-- | parsing/egramcoq.mli | 23 |
2 files changed, 3 insertions, 47 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 21a9afa29..ade31c1d3 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -9,9 +9,10 @@ open Errors open Util open Pcoq -open Extend open Constrexpr +open Notation open Notation_term +open Extend open Libnames open Names @@ -320,13 +321,6 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) | Name id -> CPatAtom (loc,Some (Ident (loc,id))) -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - type 'r env = { constrs : 'r list; constrlists : 'r list list; @@ -444,14 +438,6 @@ let make_act : type r. r target -> _ -> r gen_eval = function let env = (env.constrs, env.constrlists) in CPatNotation (loc, notation, env, []) -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in @@ -491,12 +477,3 @@ let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) - -let recover_constr_grammar ntn prec = - let filter (prec', ng) = - if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng - else None - in - match List.map_filter filter (recover_grammar_command constr_grammar) with - | [x] -> x - | _ -> assert false diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 1fe06a29d..6dda3817a 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -19,28 +19,7 @@ open Egramml (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) -(** For constr notations *) - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> notation_grammar -> unit +val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit (** Add a term notation rule to the parsing system. *) - -val recover_constr_grammar : notation -> Notation.level -> notation_grammar -(** For a declared grammar, returns the rule + the ordered entry types - of variables in the rule (for use in the interpretation) *) |