diff options
| author | Pierre-Marie Pédrot | 2015-10-27 14:08:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-27 14:08:54 +0100 |
| commit | 04b244a4ba8605a97cd96855b4c4e628ba27db7b (patch) | |
| tree | 87e9b8753bf595ef3c1852798bb995b800cbd193 | |
| parent | 72bed859fb8d037044abd8a1518661c52502f7be (diff) | |
Removing unused code in Pcoq.
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 16 |
2 files changed, 1 insertions, 16 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 4bb1fd0a49..b017fddc71 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -52,7 +52,6 @@ end (** Grammar entries with associated types *) -type entry_type = argument_type type grammar_object = Gramobj.grammar_object type typed_entry = argument_type * grammar_object G.entry let in_typed_entry t e = (t,Gramobj.weaken_entry e) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 69b25879bf..9a27b6e045 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -139,19 +139,6 @@ val grammar_extend : (** Remove the last n extensions *) val remove_grammars : int -> unit - - - -(** The type of typed grammar objects *) -type typed_entry - -(** The possible types for extensible grammars *) -type entry_type = argument_type - -val type_of_typed_entry : typed_entry -> entry_type -val object_of_typed_entry : typed_entry -> grammar_object Gram.entry -val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -171,7 +158,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.entry @@ -296,7 +282,7 @@ val interp_entry_name : bool (** true to fail on unknown entry *) -> 's target -> string -> string -> 's entry_name (** Recover the list of all known tactic notation entries. *) -val list_entry_names : unit -> (string * entry_type) list +val list_entry_names : unit -> (string * argument_type) list (** Registering/resetting the level of a constr entry *) |