diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 1b8cbe49a..23c0db5b4 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -12,9 +12,12 @@ open Util open Names open Term -open Nametab +open Declare open Library +open Libnames +open Nametab open Vernacexpr + (*i*) (*s Declaration functions. The following functions take ASTs, @@ -28,12 +31,13 @@ val declare_definition : identifier -> bool * strength -> val syntax_definition : identifier -> Coqast.t -> unit -val declare_assumption : identifier -> strength -> Coqast.t -> global_reference +val declare_assumption : identifier -> strength -> + local_binder list -> Coqast.t -> global_reference val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit val declare_mutual_with_eliminations : - Indtypes.mutual_inductive_entry -> section_path + Entries.mutual_inductive_entry -> mutual_inductive val build_recursive : (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list @@ -41,7 +45,7 @@ val build_recursive : val build_corecursive : (identifier * Coqast.t * Coqast.t) list -> unit -val build_scheme : (identifier * bool * Nametab.qualid located * Coqast.t) list -> unit +val build_scheme : (identifier * bool * qualid located * Coqast.t) list -> unit val start_proof_com : identifier option -> bool * strength -> Coqast.t -> Proof_type.declaration_hook -> unit |