From 8ff2de8c01b3ba3563517627b1f5c9eb2c4bcb77 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 14 Mar 2012 09:53:06 +0000 Subject: Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/command.mli | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'toplevel/command.mli') diff --git a/toplevel/command.mli b/toplevel/command.mli index 0adc66d56..3cced65f1 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -32,11 +32,15 @@ val set_declare_assumptions_hook : (types -> unit) -> unit val interp_definition : local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Impargs.manual_implicits + constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits -val declare_definition : identifier -> locality * definition_object_kind -> +val declare_definition : identifier -> definition_kind -> definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a +val do_definition : identifier -> definition_kind -> + local_binder list -> red_expr option -> constr_expr -> + constr_expr option -> unit declaration_hook -> unit + (** {6 Parameters/Assumptions} *) val interp_assumption : -- cgit v1.2.3