diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:50 +0200 |
| commit | 568aa9dff652d420e66cda7914d4bc265bb276e7 (patch) | |
| tree | c493eaaa87636e304f5788136a5fd1c255816821 /toplevel/command.mli | |
| parent | bce318b6d991587773ef2fb18c83de8d24bc4a5f (diff) | |
| parent | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (diff) | |
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index b97cb487d..2d27552a1 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -36,7 +36,7 @@ val interp_definition : constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits -val declare_definition : Id.t -> definition_kind -> +val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind -> Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference @@ -91,6 +91,7 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list @@ -105,6 +106,7 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) (one_inductive_expr * decl_notation list) list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit @@ -148,12 +150,13 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : + flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit -val declare_cofixpoint : locality -> polymorphic -> +val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -161,14 +164,16 @@ val declare_cofixpoint : locality -> polymorphic -> (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> +val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference |