diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 36 |
1 files changed, 4 insertions, 32 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 469e1a011..6b503a011 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,9 +51,8 @@ end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in - try - { it=(List.nth goals (i-1)) ; sigma=sigma; } + let goals,_,_,_,sigma = Proof.proof p in + try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = @@ -141,7 +140,8 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); - const, status, fst univs + let univs = UState.demote_seff_univs const univs in + const, status, univs with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); @@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> let solve_by_implicit_tactic () = match !implicit_tactic with | None -> None | Some tac -> Some (apply_implicit_tactic tac) - -(** Deprecated functions *) -let refining = Proof_global.there_are_pending_proofs -let check_no_pending_proofs = Proof_global.check_no_pending_proof - -let get_current_proof_name = Proof_global.get_current_proof_name -let get_all_proof_names = Proof_global.get_all_proof_names - -type lemma_possible_guards = Proof_global.lemma_possible_guards - -let delete_proof = Proof_global.discard -let delete_current_proof = Proof_global.discard_current -let delete_all_proofs = Proof_global.discard_all - -let get_pftreestate () = - Proof_global.give_me_the_proof () - -let set_end_tac tac = - Proof_global.set_endline_tactic tac - -let set_used_variables l = - Proof_global.set_used_variables l - -let get_used_variables () = - Proof_global.get_used_variables () - -let get_universe_decl () = - Proof_global.get_universe_decl () |