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 | |
| parent | a071ac178ee9e6ca0cbae14db24e10775b0af881 (diff) | |
Better handling of the universe context in case of Admitted proof obligations.
| -rw-r--r-- | stm/lemmas.ml | 4 | ||||
| -rw-r--r-- | stm/lemmas.mli | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 15 |
3 files changed, 13 insertions, 8 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 -> diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 8f637aa325..13f9e9339d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -834,11 +834,16 @@ let rec solve_obligation prg num tac = let obls = Array.copy obls in let _ = obls.(num) <- obl in let ctx' = - if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' - else ctx' + let ctx = + match ctx' with + | None -> prg.prg_ctx + | Some ctx' -> ctx' + in + if not (pi2 prg.prg_kind) (* Not polymorphic *) then + (* This context is already declared globally, we cannot + instantiate the rigid variables anymore *) + Evd.abstract_undefined_variables ctx + else ctx in let res = try update_obls |