diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 26 |
1 files changed, 1 insertions, 25 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index fc1727fc1..cf5174af9 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -12,7 +12,6 @@ open Extend open Vernacexpr open Genarg open Constrexpr -open Tacexpr open Libnames open Misctypes open Genredexpr @@ -179,30 +178,6 @@ module Module : val module_type : module_ast Gram.entry end -module Tactic : - sig - val open_constr : constr_expr Gram.entry - val constr_with_bindings : constr_expr with_bindings Gram.entry - val bindings : constr_expr bindings Gram.entry - val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry - val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry - val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry - val uconstr : constr_expr Gram.entry - val quantified_hypothesis : quantified_hypothesis Gram.entry - val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry - val int_or_var : int or_var Gram.entry - val red_expr : raw_red_expr Gram.entry - val simple_tactic : raw_tactic_expr Gram.entry - val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry - val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry - val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry - val tactic_arg : raw_tactic_arg Gram.entry - val tactic_expr : raw_tactic_expr Gram.entry - val binder_tactic : raw_tactic_expr Gram.entry - val tactic : raw_tactic_expr Gram.entry - val tactic_eoi : raw_tactic_expr Gram.entry - end - module Vernac_ : sig val gallina : vernac_expr Gram.entry @@ -214,6 +189,7 @@ module Vernac_ : val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry + val red_expr : raw_red_expr Gram.entry val hint_info : Vernacexpr.hint_info_expr Gram.entry end |