diff options
| author | Matthieu Sozeau | 2014-07-10 15:40:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-10 15:40:41 +0200 |
| commit | 6663052ccd613faf4282bd73121a44398bd3ba76 (patch) | |
| tree | 82d2aa5239e9a2110fb8de763f45fad98241d899 /stm | |
| parent | a071ac178ee9e6ca0cbae14db24e10775b0af881 (diff) | |
Better handling of the universe context in case of Admitted proof obligations.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 4 | ||||
| -rw-r--r-- | stm/lemmas.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5d2babaca9..fbe17b8f8b 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -336,11 +336,11 @@ let standard_proof_terminator compute_guard hook = let universe_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> - admit (hook Evd.empty_evar_universe_context) (); + admit (hook None) (); Pp.feedback Feedback.AddedAxiom | Proved (is_opaque,idopt,proof) -> let proof = get_proof proof compute_guard - (hook proof.Proof_global.universes) is_opaque in + (hook (Some proof.Proof_global.universes)) is_opaque in begin match idopt with | None -> save_named proof | Some ((_,id),None) -> save_anonymous proof id diff --git a/stm/lemmas.mli b/stm/lemmas.mli index d5a4c709e8..b77413bc9f 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -31,7 +31,7 @@ val start_proof : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Enviro val start_proof_univs : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - (Proof_global.proof_universes -> unit declaration_hook) -> unit + (Proof_global.proof_universes option -> unit declaration_hook) -> unit val start_proof_com : goal_kind -> (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list -> |