diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /vernac/obligations.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'vernac/obligations.mli')
-rw-r--r-- | vernac/obligations.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/vernac/obligations.mli b/vernac/obligations.mli index cc2cacd8..a37c30aa 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Environ open Constr open Evd open Names -open Globnames (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof @@ -49,13 +48,13 @@ type obligation_info = type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) - | Defined of global_reference (* Defined as id *) + | Defined of GlobRef.t (* Defined as id *) val default_tactic : unit Proofview.tactic ref val add_definition : Names.Id.t -> ?term:constr -> types -> UState.t -> - ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) + ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -63,17 +62,17 @@ val add_definition : Names.Id.t -> ?term:constr -> types -> ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = - (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list | IsCoFixpoint val add_mutual_definitions : (Names.Id.t * constr * types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> UState.t -> - ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) + ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> |