diff options
| author | Pierre-Marie Pédrot | 2016-06-17 18:25:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 18:54:43 +0200 |
| commit | 53ced0735f7e24735d78a02fc74588b8d9186eab (patch) | |
| tree | 93661920f42d9be934e59f5f972d165ea24785b7 /toplevel/command.mli | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 2d27552a19..a5132cc664 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 : flags:Declarations.typing_flags -> Id.t -> definition_kind -> +val declare_definition : 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 @@ -150,13 +150,12 @@ 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 : flags:Declarations.typing_flags -> locality -> polymorphic -> +val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -164,16 +163,16 @@ val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorp (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - flags:Declarations.typing_flags -> (* When [false], assume guarded. *) + (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - flags:Declarations.typing_flags -> (* When [false], assume guarded. *) + (* 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 : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> +val declare_fix : ?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 |