diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index eb49b403c..b4a5bc9a7 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -175,8 +175,7 @@ module Tactic : module Vernac_ : sig - open Util - open Libnames + open Decl_kinds val thm_token : theorem_kind Gram.Entry.e val class_rawexpr : class_rawexpr Gram.Entry.e val gallina : vernac_expr Gram.Entry.e @@ -185,7 +184,4 @@ module Vernac_ : val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e val vernac_eoi : vernac_expr Gram.Entry.e -(* - val reduce : Coqast.t list Gram.Entry.e -*) end |