diff options
Diffstat (limited to 'toplevel/obligations.mli')
| -rw-r--r-- | toplevel/obligations.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 746b4ed14..f03e6c446 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -17,7 +17,7 @@ open Decl_kinds open Tacexpr (** Forward declaration. *) -val declare_fix_ref : (definition_kind -> Id.t -> +val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : @@ -64,6 +64,7 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op val get_proofs_transparency : unit -> bool val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> + Univ.universe_context_set -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -80,6 +81,7 @@ type fixpoint_kind = val add_mutual_definitions : (Names.Id.t * Term.constr * Term.types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> + Univ.universe_context_set -> ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> |