diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 26526a5f..8ac8c234 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) +(*i $Id: command.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Util @@ -56,18 +56,16 @@ val declare_assumption : identifier located list -> val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit - -val compute_interning_datas : Environ.env -> - 'a list -> - 'b list -> - Term.types list -> - Impargs.manual_explicitation list list -> +val compute_interning_datas : Environ.env -> 'a list -> 'b list -> + Term.types list ->Impargs.manual_explicitation list list -> 'a list * - ('b * - (Names.identifier list * Impargs.implicits_list * - Topconstr.scope_name option list)) + ('b * (Names.identifier list * Impargs.implicits_list * + Topconstr.scope_name option list)) list +val check_mutuality : Environ.env -> definition_object_kind -> + (identifier * types) list -> unit + val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : @@ -87,10 +85,10 @@ type fixpoint_expr = { fix_type : constr_expr } -val recursive_message : Decl_kinds.definition_object_kind -> - int array option -> Names.identifier list -> Pp.std_ppcmds +val recursive_message : definition_object_kind -> + int array option -> identifier list -> Pp.std_ppcmds -val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier -> +val declare_fix : bool -> definition_object_kind -> identifier -> constr -> types -> Impargs.manual_explicitation list -> global_reference val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit |